ficystodraunju lujvo

x1 is an injective function (distinctness-preserving function) from x2 (domain) to x3 (codomain).

This is a brapagjvo (one of its veljvo is the zi'evla "stodraunju"). Let f be the sumti which fills x1; for any y and z in x2, y =/= z iff f(y) =/= f(z).

In notes:

atfau'u
x1 is a bijective function / isomorphism from x2 to x3, with inverse x4, in system / category x5; x1 has an inverse; x1 is a function that is injective and surjective; x2 and x3 are isomorphic; x1 is invertible.
fatfrika'efancu
x1=fan1=fr1 is a bijective function / isomorphism from x2=fan2 to x3=fan3, with inverse x4, in system / category x5; x1 has an inverse; x1 is a function that is injective and surjective; x2 and x3 are isomorphic; x1 is invertible.
stodraunju
x1 is a function mapping x2 (domain) to x3 (codomain) such that properties x4 (ka) of x2 are preserved in its image under x1 according to the rules/operations/relations of x3 corresponding to those of x2 by x1.