let L1, L2, L3 be RelStr ; for f being Function of L1,L2 st f is isomorphic holds
for g being Function of L2,L3 st g is isomorphic holds
for h being Function of L1,L3 st h = g * f holds
h is isomorphic
let f1 be Function of L1,L2; ( f1 is isomorphic implies for g being Function of L2,L3 st g is isomorphic holds
for h being Function of L1,L3 st h = g * f1 holds
h is isomorphic )
assume A1:
f1 is isomorphic
; for g being Function of L2,L3 st g is isomorphic holds
for h being Function of L1,L3 st h = g * f1 holds
h is isomorphic
let f2 be Function of L2,L3; ( f2 is isomorphic implies for h being Function of L1,L3 st h = f2 * f1 holds
h is isomorphic )
assume A2:
f2 is isomorphic
; for h being Function of L1,L3 st h = f2 * f1 holds
h is isomorphic
let h be Function of L1,L3; ( h = f2 * f1 implies h is isomorphic )
assume A3:
h = f2 * f1
; h is isomorphic
per cases
( ( not L1 is empty & not L2 is empty & not L3 is empty ) or L1 is empty or L2 is empty or L3 is empty )
;
suppose
( not
L1 is
empty & not
L2 is
empty & not
L3 is
empty )
;
h is isomorphic then reconsider L1 =
L1,
L2 =
L2,
L3 =
L3 as non
empty RelStr ;
reconsider f1 =
f1 as
Function of
L1,
L2 ;
reconsider f2 =
f2 as
Function of
L2,
L3 ;
consider g1 being
Function of
L2,
L1 such that A4:
(
g1 = f1 " &
g1 is
monotone )
by A1, WAYBEL_0:def 38;
consider g2 being
Function of
L3,
L2 such that A5:
(
g2 = f2 " &
g2 is
monotone )
by A2, WAYBEL_0:def 38;
A6:
f2 * f1 is
monotone
by A1, A2, YELLOW_2:12;
(
g1 * g2 is
monotone &
g1 * g2 = (f2 * f1) " )
by A1, A2, A4, A5, FUNCT_1:44, YELLOW_2:12;
hence
h is
isomorphic
by A1, A2, A3, A6, WAYBEL_0:def 38;
verum end; end;