let S1, S2, T1, T2 be RelStr ; :: thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f being Function of S1,T1 st f is isomorphic holds
for g being Function of S2,T2 st g = f holds
g is isomorphic )
assume that
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and
A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; :: thesis: for f being Function of S1,T1 st f is isomorphic holds
for g being Function of S2,T2 st g = f holds
g is isomorphic
let f be Function of S1,T1; :: thesis: ( f is isomorphic implies for g being Function of S2,T2 st g = f holds
g is isomorphic )
assume A3: f is isomorphic ; :: thesis: for g being Function of S2,T2 st g = f holds
g is isomorphic
let g be Function of S2,T2; :: thesis: ( g = f implies g is isomorphic )
assume A4: g = f ; :: thesis: g is isomorphic
per cases ( S1 is empty or not S1 is empty ) ;
suppose A5: S1 is empty ; :: thesis: g is isomorphic
then T1 is empty by A3, WAYBEL_0:def 38;
then A6: T2 is empty by A2;
S2 is empty by A1, A5;
hence g is isomorphic by A6, WAYBEL_0:def 38; :: thesis: verum
end;
suppose not S1 is empty ; :: thesis: g is isomorphic
then reconsider S1 = S1, T1 = T1 as non empty RelStr by A3, WAYBEL_0:def 38;
reconsider f = f as Function of S1,T1 ;
( the carrier of S1 <> {} & the carrier of T1 <> {} ) ;
then reconsider S2 = S2, T2 = T2 as non empty RelStr by A1, A2;
reconsider g = g as Function of S2,T2 ;
A7: now :: thesis: for x, y being Element of S2 holds
( x <= y iff g . x <= g . y )
let x, y be Element of S2; :: thesis: ( x <= y iff g . x <= g . y )
reconsider a = x, b = y as Element of S1 by A1;
A8: ( x <= y iff a <= b ) by A1, YELLOW_0:1;
( g . x <= g . y iff f . a <= f . b ) by A2, A4, YELLOW_0:1;
hence ( x <= y iff g . x <= g . y ) by A3, A8, WAYBEL_0:66; :: thesis: verum
end;
rng f = the carrier of T1 by A3, WAYBEL_0:66;
hence g is isomorphic by A2, A3, A4, A7, WAYBEL_0:66; :: thesis: verum
end;
end;