defpred S₁[ set ] means ( ( for s being stack of F₁() st emp s holds
[s,F₄()] in $1 ) & ( for s being stack of F₁()
for a being Element of F₁()
for v being Element of F₃() st [s,v] in $1 holds
[(push (a,s)),F₅(a,v)] in $1 ) );
consider M being set such that
A1: for x being set holds
( x in M iff ( x in bool [: the carrier' of F₁(),F₃():] & S₁[x] ) ) from XFAMILY:sch 1();
A2: ( S₁[[: the carrier' of F₁(),F₃():]] & [: the carrier' of F₁(),F₃():] in bool [: the carrier' of F₁(),F₃():] ) by ZFMISC_1:def 1;
then A3: [: the carrier' of F₁(),F₃():] in M by A1;
reconsider M = M as non empty set by A1, A2;
set F = meet M;
reconsider F = meet M as Subset of [: the carrier' of F₁(),F₃():] by A3, SETFAM_1:3;
defpred S₂[ stack of F₁()] means for y1, y2 being object st [$1,y1] in F & [$1,y2] in F holds
y1 = y2;
A4: S₁[F]

hereby :: thesis:

let s be stack of F₁(); :: thesis:
assume emp s ; :: thesis:
then for Y being set st Y in M holds
[s,F₄()] in Y by A1;
hence [s,F₄()] in F by SETFAM_1:def 1; :: thesis:

end;

let s be stack of F₁(); :: thesis:
let a be Element of F₁(); :: thesis:
let v be Element of F₃(); :: thesis:
assume A5: [s,v] in F ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume Y in M ; :: thesis:
then ( S₁[Y] & [s,v] in Y ) by A5, A1, SETFAM_1:def 1;
hence [(push (a,s)),F₅(a,v)] in Y ; :: thesis:

end;

hence [(push (a,s)),F₅(a,v)] in F by SETFAM_1:def 1; :: thesis:

end;

defpred S₃[ stack of F₁()] means ex y being set st [$1,y] in F;
A6: for s being stack of F₁() st emp s holds
S₃[s]

proof

let s be stack of F₁(); :: thesis:
assume A7: emp s ; :: thesis:
take y = F₄(); :: thesis:
for Y being set st Y in M holds
[s,F₄()] in Y by A7, A1;
hence [s,y] in F by SETFAM_1:def 1; :: thesis:

end;

A8: for s being stack of F₁()
for e being Element of F₁() st S₃[s] holds
S₃[ push (e,s)]

proof

let s be stack of F₁(); :: thesis:
let e be Element of F₁(); :: thesis:
given y being set such that A9: [s,y] in F ; :: thesis:
reconsider y = y as Element of F₃() by A9, ZFMISC_1:87;
take z = F₅(e,y); :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume A10: Y in M ; :: thesis:
then [s,y] in Y by A9, SETFAM_1:def 1;
hence [(push (e,s)),z] in Y by A10, A1; :: thesis:

end;

hence [(push (e,s)),z] in F by SETFAM_1:def 1; :: thesis:

end;

A11: for s being stack of F₁() st emp s holds
S₂[s]

proof

let s be stack of F₁(); :: thesis:
assume A12: emp s ; :: thesis:
let y1, y2 be object ; :: thesis:
assume A13: ( [s,y1] in F & [s,y2] in F ) ; :: thesis:
set Y1 = F \ {[s,y1]};
set Y2 = F \ {[s,y2]};

A14: now :: thesis:

assume A15: y1 <> F₄() ; :: thesis:
S₁[F \ {[s,y1]}]

proof

hereby :: thesis:

let s1 be stack of F₁(); :: thesis:
assume emp s1 ; :: thesis:
then A16: [s1,F₄()] in F by A4;
[s,y1] <> [s1,F₄()] by A15, XTUPLE_0:1;
then [s1,F₄()] nin {[s,y1]} by TARSKI:def 1;
hence [s1,F₄()] in F \ {[s,y1]} by A16, XBOOLE_0:def 5; :: thesis:

end;

let s1 be stack of F₁(); :: thesis:
let a be Element of F₁(); :: thesis:
let v be Element of F₃(); :: thesis:
assume [s1,v] in F \ {[s,y1]} ; :: thesis:
then [s1,v] in F by XBOOLE_0:def 5;
then A17: [(push (a,s1)),F₅(a,v)] in F by A4;
push (a,s1) <> s by A12, Def12;
then [s,y1] <> [(push (a,s1)),F₅(a,v)] by XTUPLE_0:1;
then [(push (a,s1)),F₅(a,v)] nin {[s,y1]} by TARSKI:def 1;
hence [(push (a,s1)),F₅(a,v)] in F \ {[s,y1]} by A17, XBOOLE_0:def 5; :: thesis:

end;

then F \ {[s,y1]} in M by A1;
then F c= F \ {[s,y1]} by SETFAM_1:3;
then ( [s,y1] in F \ {[s,y1]} & [s,y1] in {[s,y1]} ) by A13, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

now :: thesis:

assume A18: y2 <> F₄() ; :: thesis:
S₁[F \ {[s,y2]}]

proof

hereby :: thesis:

let s1 be stack of F₁(); :: thesis:
assume emp s1 ; :: thesis:
then A19: [s1,F₄()] in F by A4;
[s,y2] <> [s1,F₄()] by A18, XTUPLE_0:1;
then [s1,F₄()] nin {[s,y2]} by TARSKI:def 1;
hence [s1,F₄()] in F \ {[s,y2]} by A19, XBOOLE_0:def 5; :: thesis:

end;

let s1 be stack of F₁(); :: thesis:
let a be Element of F₁(); :: thesis:
let v be Element of F₃(); :: thesis:
assume [s1,v] in F \ {[s,y2]} ; :: thesis:
then [s1,v] in F by XBOOLE_0:def 5;
then A20: [(push (a,s1)),F₅(a,v)] in F by A4;
push (a,s1) <> s by A12, Def12;
then [s,y2] <> [(push (a,s1)),F₅(a,v)] by XTUPLE_0:1;
then [(push (a,s1)),F₅(a,v)] nin {[s,y2]} by TARSKI:def 1;
hence [(push (a,s1)),F₅(a,v)] in F \ {[s,y2]} by A20, XBOOLE_0:def 5; :: thesis:

end;

then F \ {[s,y2]} in M by A1;
then F c= F \ {[s,y2]} by SETFAM_1:3;
then ( [s,y2] in F \ {[s,y2]} & [s,y2] in {[s,y2]} ) by A13, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

hence y1 = y2 by A14; :: thesis:

end;

A21: for s being stack of F₁()
for e being Element of F₁() st S₂[s] holds
S₂[ push (e,s)]

proof

let s be stack of F₁(); :: thesis:
let e be Element of F₁(); :: thesis:
assume A22: S₂[s] ; :: thesis:
let y1, y2 be object ; :: thesis:
assume A23: ( [(push (e,s)),y1] in F & [(push (e,s)),y2] in F ) ; :: thesis:
S₃[s] from STACKS_1:sch 3(A6, A8);
then consider y being set such that
A24: [s,y] in F ;
reconsider y = y as Element of F₃() by A24, ZFMISC_1:87;
set Y1 = F \ {[(push (e,s)),y1]};
set Y2 = F \ {[(push (e,s)),y2]};

A25: now :: thesis:

assume A26: y1 <> F₅(e,y) ; :: thesis:
S₁[F \ {[(push (e,s)),y1]}]

proof

hereby :: thesis:

let s1 be stack of F₁(); :: thesis:
assume A27: emp s1 ; :: thesis:
then A28: [s1,F₄()] in F by A4;
not emp push (e,s) by Def12;
then [(push (e,s)),y1] <> [s1,F₄()] by A27, XTUPLE_0:1;
then [s1,F₄()] nin {[(push (e,s)),y1]} by TARSKI:def 1;
hence [s1,F₄()] in F \ {[(push (e,s)),y1]} by A28, XBOOLE_0:def 5; :: thesis:

end;

let s1 be stack of F₁(); :: thesis:
let a be Element of F₁(); :: thesis:
let v be Element of F₃(); :: thesis:
assume [s1,v] in F \ {[(push (e,s)),y1]} ; :: thesis:
then A29: [s1,v] in F by XBOOLE_0:def 5;
then A30: [(push (a,s1)),F₅(a,v)] in F by A4;

now :: thesis:

assume [(push (e,s)),y1] = [(push (a,s1)),F₅(a,v)] ; :: thesis:
then A31: ( push (e,s) = push (a,s1) & y1 = F₅(a,v) ) by XTUPLE_0:1;
then ( e = a & s = s1 ) by Th3;
hence contradiction by A22, A24, A29, A26, A31; :: thesis:

end;

then [(push (a,s1)),F₅(a,v)] nin {[(push (e,s)),y1]} by TARSKI:def 1;
hence [(push (a,s1)),F₅(a,v)] in F \ {[(push (e,s)),y1]} by A30, XBOOLE_0:def 5; :: thesis:

end;

then F \ {[(push (e,s)),y1]} in M by A1;
then F c= F \ {[(push (e,s)),y1]} by SETFAM_1:3;
then ( [(push (e,s)),y1] in F \ {[(push (e,s)),y1]} & [(push (e,s)),y1] in {[(push (e,s)),y1]} ) by A23, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

now :: thesis:

assume A32: y2 <> F₅(e,y) ; :: thesis:
S₁[F \ {[(push (e,s)),y2]}]

proof

hereby :: thesis:

let s1 be stack of F₁(); :: thesis:
assume A33: emp s1 ; :: thesis:
then A34: [s1,F₄()] in F by A4;
not emp push (e,s) by Def12;
then [(push (e,s)),y2] <> [s1,F₄()] by A33, XTUPLE_0:1;
then [s1,F₄()] nin {[(push (e,s)),y2]} by TARSKI:def 1;
hence [s1,F₄()] in F \ {[(push (e,s)),y2]} by A34, XBOOLE_0:def 5; :: thesis:

end;

let s1 be stack of F₁(); :: thesis:
let a be Element of F₁(); :: thesis:
let v be Element of F₃(); :: thesis:
assume [s1,v] in F \ {[(push (e,s)),y2]} ; :: thesis:
then A35: [s1,v] in F by XBOOLE_0:def 5;
then A36: [(push (a,s1)),F₅(a,v)] in F by A4;

now :: thesis:

assume [(push (e,s)),y2] = [(push (a,s1)),F₅(a,v)] ; :: thesis:
then A37: ( push (e,s) = push (a,s1) & y2 = F₅(a,v) ) by XTUPLE_0:1;
then ( e = a & s = s1 ) by Th3;
hence contradiction by A22, A24, A35, A32, A37; :: thesis:

end;

then [(push (a,s1)),F₅(a,v)] nin {[(push (e,s)),y2]} by TARSKI:def 1;
hence [(push (a,s1)),F₅(a,v)] in F \ {[(push (e,s)),y2]} by A36, XBOOLE_0:def 5; :: thesis:

end;

then F \ {[(push (e,s)),y2]} in M by A1;
then F c= F \ {[(push (e,s)),y2]} by SETFAM_1:3;
then ( [(push (e,s)),y2] in F \ {[(push (e,s)),y2]} & [(push (e,s)),y2] in {[(push (e,s)),y2]} ) by A23, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

hence y1 = y2 by A25; :: thesis:

end;

A38: F is Function-like

proof

let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis:
assume A39: ( [x,y1] in F & [x,y2] in F ) ; :: thesis:
then reconsider x = x as stack of F₁() by ZFMISC_1:87;
S₂[x] from STACKS_1:sch 3(A11, A21);
hence y1 = y2 by A39; :: thesis:

end;

F is quasi_total

proof

per cases ;
:: according to FUNCT_2:def 1

case F₃() <> {} ; :: thesis:

thus the carrier' of F₁() c= dom F :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier' of F₁() ; :: thesis:
then reconsider x = x as stack of F₁() ;
S₃[x] from STACKS_1:sch 3(A6, A8);
hence x in dom F by XTUPLE_0:def 12; :: thesis:

end;

thus dom F c= the carrier' of F₁() ; :: thesis:

end;

case F₃() = {} ; :: thesis:

hence F = {} ; :: thesis:

end;

then reconsider F = F as Function of the carrier' of F₁(),F₃() by A38;
take a = F . F₂(); :: thesis:
take F ; :: thesis:
thus a = F . F₂() ; :: thesis:

hereby :: thesis:

let s1 be stack of F₁(); :: thesis:
assume emp s1 ; :: thesis:
then [s1,F₄()] in F by A4;
hence F . s1 = F₄() by FUNCT_1:1; :: thesis:

end;

let s1 be stack of F₁(); :: thesis:
let e be Element of F₁(); :: thesis:
dom F = the carrier' of F₁() by FUNCT_2:def 1;
then [s1,(F . s1)] in F by FUNCT_1:def 2;
then [(push (e,s1)),F₅(e,(F . s1))] in F by A4;
hence F . (push (e,s1)) = F₅(e,(F . s1)) by FUNCT_1:1; :: thesis: