let A be non empty set ; :: thesis: for f, g being Permutation of A

for R being Relation of [:A,A:] st R is_transitive_in [:A,A:] & 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 R is_transitive_in [:A,A:] & 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: ( R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R implies f * g is_FormalIz_of R )

assume that

A1: for x, y, z being object st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds

[x,z] in R and

A2: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R and

A3: for x, y being Element of A holds [[x,y],[(g . x),(g . y)]] in R ; :: according to RELAT_2:def 8,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:15;

then A4: [[(g . x),(g . y)],[((f * g) . x),((f * g) . y)]] in R by A2;

A5: [((f * g) . x),((f * g) . y)] in [:A,A:] by ZFMISC_1:def 2;

A6: ( [x,y] in [:A,A:] & [(g . x),(g . y)] in [:A,A:] ) by ZFMISC_1:def 2;

[[x,y],[(g . x),(g . y)]] in R by A3;

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

for R being Relation of [:A,A:] st R is_transitive_in [:A,A:] & 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 R is_transitive_in [:A,A:] & 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: ( R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R implies f * g is_FormalIz_of R )

assume that

A1: for x, y, z being object st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds

[x,z] in R and

A2: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R and

A3: for x, y being Element of A holds [[x,y],[(g . x),(g . y)]] in R ; :: according to RELAT_2:def 8,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:15;

then A4: [[(g . x),(g . y)],[((f * g) . x),((f * g) . y)]] in R by A2;

A5: [((f * g) . x),((f * g) . y)] in [:A,A:] by ZFMISC_1:def 2;

A6: ( [x,y] in [:A,A:] & [(g . x),(g . y)] in [:A,A:] ) by ZFMISC_1:def 2;

[[x,y],[(g . x),(g . y)]] in R by A3;

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