let R1, R2, R3 be non empty RelStr ; :: thesis: for f1 being Function of R1,R3 st f1 is isomorphic holds

for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

let f1 be Function of R1,R3; :: thesis: ( f1 is isomorphic implies for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )

assume A1: f1 is isomorphic ; :: thesis: for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

let f2 be Function of R2,R3; :: thesis: ( f2 = f1 & f2 is isomorphic implies RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )

assume that

A2: f2 = f1 and

A3: f2 is isomorphic ; :: thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

A4: the carrier of R1 = rng (f2 ") by A1, A2, WAYBEL_0:67

.= the carrier of R2 by A3, WAYBEL_0:67 ;

A5: the InternalRel of R2 c= the InternalRel of R1

for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

let f1 be Function of R1,R3; :: thesis: ( f1 is isomorphic implies for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )

assume A1: f1 is isomorphic ; :: thesis: for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

let f2 be Function of R2,R3; :: thesis: ( f2 = f1 & f2 is isomorphic implies RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )

assume that

A2: f2 = f1 and

A3: f2 is isomorphic ; :: thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

A4: the carrier of R1 = rng (f2 ") by A1, A2, WAYBEL_0:67

.= the carrier of R2 by A3, WAYBEL_0:67 ;

A5: the InternalRel of R2 c= the InternalRel of R1

proof

the InternalRel of R1 c= the InternalRel of R2
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in the InternalRel of R2 or [x1,x2] in the InternalRel of R1 )

assume A6: [x1,x2] in the InternalRel of R2 ; :: thesis: [x1,x2] in the InternalRel of R1

then reconsider x19 = x1, x29 = x2 as Element of R2 by ZFMISC_1:87;

reconsider y1 = x19, y2 = x29 as Element of R1 by A4;

x19 <= x29 by A6, ORDERS_2:def 5;

then f2 . x19 <= f2 . x29 by A3, WAYBEL_0:66;

then y1 <= y2 by A1, A2, WAYBEL_0:66;

hence [x1,x2] in the InternalRel of R1 by ORDERS_2:def 5; :: thesis: verum

end;assume A6: [x1,x2] in the InternalRel of R2 ; :: thesis: [x1,x2] in the InternalRel of R1

then reconsider x19 = x1, x29 = x2 as Element of R2 by ZFMISC_1:87;

reconsider y1 = x19, y2 = x29 as Element of R1 by A4;

x19 <= x29 by A6, ORDERS_2:def 5;

then f2 . x19 <= f2 . x29 by A3, WAYBEL_0:66;

then y1 <= y2 by A1, A2, WAYBEL_0:66;

hence [x1,x2] in the InternalRel of R1 by ORDERS_2:def 5; :: thesis: verum

proof

hence
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
by A4, A5, XBOOLE_0:def 10; :: thesis: verum
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in the InternalRel of R1 or [x1,x2] in the InternalRel of R2 )

assume A7: [x1,x2] in the InternalRel of R1 ; :: thesis: [x1,x2] in the InternalRel of R2

then reconsider x19 = x1, x29 = x2 as Element of R1 by ZFMISC_1:87;

reconsider y1 = x19, y2 = x29 as Element of R2 by A4;

x19 <= x29 by A7, ORDERS_2:def 5;

then f1 . x19 <= f1 . x29 by A1, WAYBEL_0:66;

then y1 <= y2 by A2, A3, WAYBEL_0:66;

hence [x1,x2] in the InternalRel of R2 by ORDERS_2:def 5; :: thesis: verum

end;assume A7: [x1,x2] in the InternalRel of R1 ; :: thesis: [x1,x2] in the InternalRel of R2

then reconsider x19 = x1, x29 = x2 as Element of R1 by ZFMISC_1:87;

reconsider y1 = x19, y2 = x29 as Element of R2 by A4;

x19 <= x29 by A7, ORDERS_2:def 5;

then f1 . x19 <= f1 . x29 by A1, WAYBEL_0:66;

then y1 <= y2 by A2, A3, WAYBEL_0:66;

hence [x1,x2] in the InternalRel of R2 by ORDERS_2:def 5; :: thesis: verum