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
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 ) ; :: 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 ;
consider g2 being Function of L3,L2 such that
A5: ( g2 = f2 " & g2 is monotone ) by ;
A6: f2 * f1 is monotone by ;
( g1 * g2 is monotone & g1 * g2 = (f2 * f1) " ) by ;
hence h is isomorphic by ; :: thesis: verum
end;
suppose A7: L1 is empty ; :: thesis: h is isomorphic
end;
suppose L2 is empty ; :: thesis: h is isomorphic
end;
suppose A8: L3 is empty ; :: thesis: h is isomorphic
end;
end;