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 )

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

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 that
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;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

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