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
.= the carrier of R2 by ;
A5: the InternalRel of R2 c= the InternalRel of R1
proof
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 ;
then f2 . x19 <= f2 . x29 by ;
then y1 <= y2 by ;
hence [x1,x2] in the InternalRel of R1 by ORDERS_2:def 5; :: thesis: verum
end;
the InternalRel of R1 c= the InternalRel of R2
proof
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 ;
then f1 . x19 <= f1 . x29 by ;
then y1 <= y2 by ;
hence [x1,x2] in the InternalRel of R2 by ORDERS_2:def 5; :: thesis: verum
end;
hence RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by ; :: thesis: verum