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 A1: ( 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 #) ) ; :: 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 A2: 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 A3: g = f ; :: thesis: g is isomorphic

per cases ( S1 is empty or not S1 is empty ) ;

suppose S1 is empty ; :: thesis: g is isomorphic

then ( S1 is empty & T1 is empty ) by A2, WAYBEL_0:def 38;
then ( the carrier of S2 = {} & the carrier of T2 = {} ) by A1;
then ( S2 is empty & T2 is empty ) ;
hence g is isomorphic by 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 A2, WAYBEL_0:def 38;
( the carrier of S1 <> {} & the carrier of T1 <> {} ) ;
then reconsider S2 = S2, T2 = T2 as non empty RelStr by A1;
reconsider f = f as Function of S1,T1 ;
reconsider g = g as Function of S2,T2 ;
A4: ( f is one-to-one & rng f = the carrier of T1 & ( for x, y being Element of S1 holds
( x <= y iff f . x <= f . y ) ) ) by A2, WAYBEL_0:66;

now

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;
( ( x <= y implies a <= b ) & ( a <= b implies x <= y ) & ( g . x <= g . y implies f . a <= f . b ) & ( f . a <= f . b implies g . x <= g . y ) ) by A1, A3, YELLOW_0:1;
hence ( x <= y iff g . x <= g . y ) by A2, WAYBEL_0:66; :: thesis: verum

end;

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

end;

end;