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
end;
suppose not S1 is empty ; :: thesis: g is isomorphic
then reconsider S1 = S1, T1 = T1 as non empty RelStr by ;
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 ;
( g . x <= g . y iff f . a <= f . b ) by ;
hence ( x <= y iff g . x <= g . y ) by ; :: thesis: verum
end;
rng f = the carrier of T1 by ;
hence g is isomorphic by ; :: thesis: verum
end;
end;