let R1, R2, R3 be non empty RelStr ; 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; ( 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
; 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; ( 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
; 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
let x1,
x2 be
object ;
RELAT_1:def 3 ( 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
;
[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;
verum
end;
the InternalRel of R1 c= the InternalRel of R2
proof
let x1,
x2 be
object ;
RELAT_1:def 3 ( 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
;
[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;
verum
end;
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; verum