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 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;
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;
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;
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;
end;