let X1, X2, X3 be StackAlgebra; :: thesis: for F1, F2, G1, G2 being Function st F1,G1 form_isomorphism_between X1,X2 & F2,G2 form_isomorphism_between X2,X3 holds
F2 * F1,G2 * G1 form_isomorphism_between X1,X3
let F1, F2, G1, G2 be Function; :: thesis: ( F1,G1 form_isomorphism_between X1,X2 & F2,G2 form_isomorphism_between X2,X3 implies F2 * F1,G2 * G1 form_isomorphism_between X1,X3 )
assume that
A1: ( dom F1 = the carrier of X1 & rng F1 = the carrier of X2 & F1 is one-to-one ) and
A2: ( dom G1 = the carrier' of X1 & rng G1 = the carrier' of X2 & G1 is one-to-one ) and
A3: for s1 being stack of X1
for s2 being stack of X2 st s2 = G1 . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G1 . (pop s1) & top s2 = F1 . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X2 st e2 = F1 . e1 holds
push (e2,s2) = G1 . (push (e1,s1)) ) ) and
A4: ( dom F2 = the carrier of X2 & rng F2 = the carrier of X3 & F2 is one-to-one ) and
A5: ( dom G2 = the carrier' of X2 & rng G2 = the carrier' of X3 & G2 is one-to-one ) and
A6: for s1 being stack of X2
for s2 being stack of X3 st s2 = G2 . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G2 . (pop s1) & top s2 = F2 . (top s1) ) ) & ( for e1 being Element of X2
for e2 being Element of X3 st e2 = F2 . e1 holds
push (e2,s2) = G2 . (push (e1,s1)) ) ) ; :: according to STACKS_1:def 21 :: thesis: F2 * F1,G2 * G1 form_isomorphism_between X1,X3
thus ( dom (F2 * F1) = the carrier of X1 & rng (F2 * F1) = the carrier of X3 & F2 * F1 is one-to-one ) by A1, A4, RELAT_1:27, RELAT_1:28; :: according to STACKS_1:def 21 :: thesis: ( dom (G2 * G1) = the carrier' of X1 & rng (G2 * G1) = the carrier' of X3 & G2 * G1 is one-to-one & ( for s1 being stack of X1
for s2 being stack of X3 st s2 = (G2 * G1) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) ) ) )
thus ( dom (G2 * G1) = the carrier' of X1 & rng (G2 * G1) = the carrier' of X3 & G2 * G1 is one-to-one ) by A2, A5, RELAT_1:27, RELAT_1:28; :: thesis: for s1 being stack of X1
for s2 being stack of X3 st s2 = (G2 * G1) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) )
let s1 be stack of X1; :: thesis: for s2 being stack of X3 st s2 = (G2 * G1) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) )
let s2 be stack of X3; :: thesis: ( s2 = (G2 * G1) . s1 implies ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) ) )
reconsider s3 = G1 . s1 as stack of X2 by A2, FUNCT_1:def 3;
assume s2 = (G2 * G1) . s1 ; :: thesis: ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) )
then A7: s2 = G2 . s3 by A2, FUNCT_1:13;
( emp s1 iff emp s3 ) by A3;
hence ( emp s1 iff emp s2 ) by A6, A7; :: thesis: ( not emp s1 iff ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) )

hereby :: thesis: for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1))

assume not emp s1 ; :: thesis: ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) )
then ( pop s3 = G1 . (pop s1) & top s3 = F1 . (top s1) & not emp s3 ) by A3;
then ( pop s2 = G2 . (G1 . (pop s1)) & top s2 = F2 . (F1 . (top s1)) ) by A6, A7;
hence ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) by A1, A2, FUNCT_1:13; :: thesis: verum

end;

let e1 be Element of X1; :: thesis: for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1))
let e2 be Element of X3; :: thesis: ( e2 = (F2 * F1) . e1 implies push (e2,s2) = (G2 * G1) . (push (e1,s1)) )
reconsider e3 = F1 . e1 as Element of X2 by A1, FUNCT_1:def 3;
assume e2 = (F2 * F1) . e1 ; :: thesis: push (e2,s2) = (G2 * G1) . (push (e1,s1))
then A8: e2 = F2 . e3 by A1, FUNCT_1:13;
push (e3,s3) = G1 . (push (e1,s1)) by A3;
then push (e2,s2) = G2 . (G1 . (push (e1,s1))) by A7, A8, A6;
hence push (e2,s2) = (G2 * G1) . (push (e1,s1)) by A2, FUNCT_1:13; :: thesis: verum