let A be non empty set ; :: thesis: for f, g being Permutation of A
for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds
[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R holds
f * g is_FormalIz_of R
let f, g be Permutation of A; :: thesis: for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds
[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R holds
f * g is_FormalIz_of R
let R be Relation of [:A,A:]; :: thesis: ( ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds
[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R implies f * g is_FormalIz_of R )
assume that
A1: for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds
[[x,y],[z,t]] in R and
A2: for x, y, z being Element of A holds [[x,x],[y,z]] in R and
A3: ( ( for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ) & ( for x, y being Element of A holds [[x,y],[(g . x),(g . y)]] in R ) ) ; :: according to TRANSGEO:def 2 :: thesis: f * g is_FormalIz_of R
let x be Element of A; :: according to TRANSGEO:def 2 :: thesis: for y being Element of A holds [[x,y],[((f * g) . x),((f * g) . y)]] in R
let y be Element of A; :: thesis: [[x,y],[((f * g) . x),((f * g) . y)]] in R
( f . (g . x) = (f * g) . x & f . (g . y) = (f * g) . y ) by FUNCT_2:21;
then A4: ( [[x,y],[(g . x),(g . y)]] in R & [[(g . x),(g . y)],[((f * g) . x),((f * g) . y)]] in R & [x,y] in [:A,A:] & [(g . x),(g . y)] in [:A,A:] & [((f * g) . x),((f * g) . y)] in [:A,A:] ) by A3, ZFMISC_1:def 2;

now

assume g . x = g . y ; :: thesis: [[x,y],[((f * g) . x),((f * g) . y)]] in R
then x = y by FUNCT_2:85;
hence [[x,y],[((f * g) . x),((f * g) . y)]] in R by A2; :: thesis: verum

end;

hence [[x,y],[((f * g) . x),((f * g) . y)]] in R by A1, A4; :: thesis: verum