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

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 )
;

end;

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;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

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 ;

hence g is isomorphic by A2, A3, A4, A7, WAYBEL_0:66; :: thesis: verum

end;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 )

rng f = the carrier of T1
by A3, WAYBEL_0:66;( 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;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

hence g is isomorphic by A2, A3, A4, A7, WAYBEL_0:66; :: thesis: verum