let R, S, T be Relation; :: thesis: for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of S,T holds
G * F is_isomorphism_of R,T
let F, G be Function; :: thesis: ( F is_isomorphism_of R,S & G is_isomorphism_of S,T implies G * F is_isomorphism_of R,T )
assume that
A1: dom F = field R and
A2: rng F = field S and
A3: F is one-to-one and
A4: for a, b being object holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ; :: according to WELLORD1:def 7 :: thesis: ( not G is_isomorphism_of S,T or G * F is_isomorphism_of R,T )
assume that
A5: dom G = field S and
A6: rng G = field T and
A7: G is one-to-one and
A8: for a, b being object holds
( [a,b] in S iff ( a in field S & b in field S & [(G . a),(G . b)] in T ) ) ; :: according to WELLORD1:def 7 :: thesis: G * F is_isomorphism_of R,T
thus dom (G * F) = field R by A1, A2, A5, RELAT_1:27; :: according to WELLORD1:def 7 :: thesis: ( rng (G * F) = field T & G * F is one-to-one & ( for a, b being object holds
( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) ) ) )
thus rng (G * F) = field T by A2, A5, A6, RELAT_1:28; :: thesis: ( G * F is one-to-one & ( for a, b being object holds
( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) ) ) )
thus G * F is one-to-one by A3, A7; :: thesis: for a, b being object holds
( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) )
let a, b be object ; :: thesis: ( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) )
thus ( [a,b] in R implies ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) ) :: thesis: ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T implies [a,b] in R )

proof

assume A9: [a,b] in R ; :: thesis: ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T )
hence ( a in field R & b in field R ) by RELAT_1:15; :: thesis: [((G * F) . a),((G * F) . b)] in T
then A10: ( (G * F) . a = G . (F . a) & (G * F) . b = G . (F . b) ) by A1, FUNCT_1:13;
[(F . a),(F . b)] in S by A4, A9;
hence [((G * F) . a),((G * F) . b)] in T by A8, A10; :: thesis: verum

end;

assume that
A11: ( a in field R & b in field R ) and
A12: [((G * F) . a),((G * F) . b)] in T ; :: thesis: [a,b] in R
A13: ( (G * F) . a = G . (F . a) & (G * F) . b = G . (F . b) ) by A1, A11, FUNCT_1:13;
( F . a in field S & F . b in field S ) by A1, A2, A11, FUNCT_1:def 3;
then [(F . a),(F . b)] in S by A8, A12, A13;
hence [a,b] in R by A4, A11; :: thesis: verum