let L1, L2, L3 be RelStr ; :: thesis: ( L1,L2 are_isomorphic & L2,L3 are_isomorphic implies L1,L3 are_isomorphic )
given f1 being Function of L1,L2 such that A1: f1 is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: ( not L2,L3 are_isomorphic or L1,L3 are_isomorphic )
given f2 being Function of L2,L3 such that A2: f2 is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: L1,L3 are_isomorphic
A3: ( L1 is empty implies f2 * f1 is Function of L1,L3 ) by FUNCT_2:13;

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: L1,L3 are_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;
then f2 * f1 is isomorphic by A1, A2, A6, WAYBEL_0:def 38;
hence L1,L3 are_isomorphic ; :: thesis: verum

end;

suppose A7: L1 is empty ; :: thesis: L1,L3 are_isomorphic

then reconsider f = f2 * f1 as Function of L1,L3 by A3;
L2 is empty by A1, A7, WAYBEL_0:def 38;
then L3 is empty by A2, WAYBEL_0:def 38;
then f is isomorphic by A7, WAYBEL_0:def 38;
hence L1,L3 are_isomorphic ; :: thesis: verum

end;

suppose A8: L2 is empty ; :: thesis: L1,L3 are_isomorphic

then reconsider f = f2 * f1 as Function of L1,L3 by A1, A3, WAYBEL_0:def 38;
( L1 is empty & L3 is empty ) by A1, A2, A8, WAYBEL_0:def 38;
then f is isomorphic by WAYBEL_0:def 38;
hence L1,L3 are_isomorphic ; :: thesis: verum

end;

suppose A9: L3 is empty ; :: thesis: L1,L3 are_isomorphic

then A10: L2 is empty by A2, WAYBEL_0:def 38;
then reconsider f = f2 * f1 as Function of L1,L3 by A1, A3, WAYBEL_0:def 38;
L1 is empty by A1, A10, WAYBEL_0:def 38;
then f is isomorphic by A9, WAYBEL_0:def 38;
hence L1,L3 are_isomorphic ; :: thesis: verum

end;

end;