let a1, a2 be Element of F3(); ( ex F being Function of the carrier' of F1(),F3() st
( a1 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) & ex F being Function of the carrier' of F1(),F3() st
( a2 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) implies a1 = a2 )
given F1 being Function of the carrier' of F1(),F3() such that A1:
( a1 = F1 . F2() & ( for s1 being stack of F1() st emp s1 holds
F1 . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F1 . (push (e,s1)) = F5(e,(F1 . s1)) ) )
; ( for F being Function of the carrier' of F1(),F3() holds
( not a2 = F . F2() or ex s1 being stack of F1() st
( emp s1 & not F . s1 = F4() ) or ex s1 being stack of F1() ex e being Element of F1() st not F . (push (e,s1)) = F5(e,(F . s1)) ) or a1 = a2 )
given F2 being Function of the carrier' of F1(),F3() such that A2:
( a2 = F2 . F2() & ( for s1 being stack of F1() st emp s1 holds
F2 . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F2 . (push (e,s1)) = F5(e,(F2 . s1)) ) )
; a1 = a2
defpred S1[ stack of F1()] means F1 . $1 = F2 . $1;
A3:
now for s being stack of F1() st emp s holds
S1[s]let s be
stack of
F1();
( emp s implies S1[s] )assume
emp s
;
S1[s]then
(
F1 . s = F4() &
F2 . s = F4() )
by A1, A2;
hence
S1[
s]
;
verum end;
A4:
now for s being stack of F1()
for e being Element of F1() st S1[s] holds
S1[ push (e,s)]let s be
stack of
F1();
for e being Element of F1() st S1[s] holds
S1[ push (e,s)]let e be
Element of
F1();
( S1[s] implies S1[ push (e,s)] )assume
S1[
s]
;
S1[ push (e,s)]then
F1 . (push (e,s)) = F5(
e,
(F2 . s))
by A1;
hence
S1[
push (
e,
s)]
by A2;
verum end;
S1[F2()]
from STACKS_1:sch 3(A3, A4);
hence
a1 = a2
by A1, A2; verum