let X1, X2, X3 be StackAlgebra; 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; ( 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)) ) )
; STACKS_1:def 21 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; STACKS_1:def 21 ( 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; 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; 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; ( 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
; ( ( 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; ( not emp s1 iff ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) )
let e1 be Element of X1; 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; ( 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
; 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; verum