let L1, L2, L3 be RelStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( f2 is isomorphic implies for h being Function of L1,L3 st h = f2 * f1 holds

h is isomorphic )

assume A2: f2 is isomorphic ; :: thesis: for h being Function of L1,L3 st h = f2 * f1 holds

h is isomorphic

let h be Function of L1,L3; :: thesis: ( h = f2 * f1 implies h is isomorphic )

assume A3: h = f2 * f1 ; :: thesis: h is isomorphic

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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( f2 is isomorphic implies for h being Function of L1,L3 st h = f2 * f1 holds

h is isomorphic )

assume A2: f2 is isomorphic ; :: thesis: for h being Function of L1,L3 st h = f2 * f1 holds

h is isomorphic

let h be Function of L1,L3; :: thesis: ( h = f2 * f1 implies h is isomorphic )

assume A3: h = f2 * f1 ; :: thesis: 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 )
;

end;

suppose
( not L1 is empty & not L2 is empty & not L3 is empty )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

suppose A7:
L1 is empty
; :: thesis: h is isomorphic

then
L2 is empty
by A1, WAYBEL_0:def 38;

then L3 is empty by A2, WAYBEL_0:def 38;

hence h is isomorphic by A7, WAYBEL_0:def 38; :: thesis: verum

end;then L3 is empty by A2, WAYBEL_0:def 38;

hence h is isomorphic by A7, WAYBEL_0:def 38; :: thesis: verum

suppose
L2 is empty
; :: thesis: h is isomorphic

then
( L1 is empty & L3 is empty )
by A1, A2, WAYBEL_0:def 38;

hence h is isomorphic by WAYBEL_0:def 38; :: thesis: verum

end;hence h is isomorphic by WAYBEL_0:def 38; :: thesis: verum

suppose A8:
L3 is empty
; :: thesis: h is isomorphic

then
L2 is empty
by A2, WAYBEL_0:def 38;

then L1 is empty by A1, WAYBEL_0:def 38;

hence h is isomorphic by A8, WAYBEL_0:def 38; :: thesis: verum

end;then L1 is empty by A1, WAYBEL_0:def 38;

hence h is isomorphic by A8, WAYBEL_0:def 38; :: thesis: verum