let L1, L2, L3 be RelStr ; ( 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
; WAYBEL_1:def 8 ( not L2,L3 are_isomorphic or L1,L3 are_isomorphic )
given f2 being Function of L2,L3 such that A2:
f2 is isomorphic
; WAYBEL_1:def 8 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 )
;
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
;
verum end; end;