let S1, S2, T1, T2 be RelStr ; ( 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 #)
; 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; ( f is isomorphic implies for g being Function of S2,T2 st g = f holds
g is isomorphic )
assume A3:
f is isomorphic
; for g being Function of S2,T2 st g = f holds
g is isomorphic
let g be Function of S2,T2; ( g = f implies g is isomorphic )
assume A4:
g = f
; g is isomorphic
per cases
( S1 is empty or not S1 is empty )
;
suppose
not
S1 is
empty
;
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 ;
rng f = the
carrier of
T1
by A3, WAYBEL_0:66;
hence
g is
isomorphic
by A2, A3, A4, A7, WAYBEL_0:66;
verum end; end;