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 A2:
( f2 = f1 & f2 is isomorphic )
; :: thesis: RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #)
then A3: the carrier of R1 =
rng (f2 " )
by A1, WAYBEL_0:67
.=
the carrier of R2
by A2, WAYBEL_0:67
;
A4:
the InternalRel of R1 c= the InternalRel of R2
proof
let x1,
x2 be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in the InternalRel of R1 or [x1,x2] in the InternalRel of R2 )
assume A5:
[x1,x2] in the
InternalRel of
R1
;
:: thesis: [x1,x2] in the InternalRel of R2
then reconsider x1' =
x1,
x2' =
x2 as
Element of
R1 by ZFMISC_1:106;
reconsider y1 =
x1',
y2 =
x2' as
Element of
R2 by A3;
x1' <= x2'
by A5, ORDERS_2:def 9;
then
f1 . x1' <= f1 . x2'
by A1, WAYBEL_0:66;
then
y1 <= y2
by A2, WAYBEL_0:66;
hence
[x1,x2] in the
InternalRel of
R2
by ORDERS_2:def 9;
:: thesis: verum
end;
the InternalRel of R2 c= the InternalRel of R1
proof
let x1,
x2 be
set ;
:: 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 x1' =
x1,
x2' =
x2 as
Element of
R2 by ZFMISC_1:106;
reconsider y1 =
x1',
y2 =
x2' as
Element of
R1 by A3;
x1' <= x2'
by A6, ORDERS_2:def 9;
then
f2 . x1' <= f2 . x2'
by A2, WAYBEL_0:66;
then
y1 <= y2
by A1, A2, WAYBEL_0:66;
hence
[x1,x2] in the
InternalRel of
R1
by ORDERS_2:def 9;
:: thesis: verum
end;
hence
RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #)
by A3, A4, XBOOLE_0:def 10; :: thesis: verum