defpred S1[ set ] means ( ( for s being stack of F1() st emp s holds
[s,F4()] in $1 ) & ( for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in $1 holds
[(push (a,s)),F5(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 F1(),F3():] & S1[x] ) ) from XFAMILY:sch 1();
 A2: ( S1[[: the carrier' of F1(),F3():]] & [: the carrier' of F1(),F3():] in bool [: the carrier' of F1(),F3():] ) by ZFMISC_1:def 1;
then A3: [: the carrier' of F1(),F3():] 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 F1(),F3():] by A3, SETFAM_1:3;
defpred S2[ stack of F1()] means for y1, y2 being object st [$1,y1] in F & [$1,y2] in F holds
y1 = y2;
A4: S1[F]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let s be stack of F1(); :: thesis: ( emp s implies [s,F4()] in F )
assume emp s ; :: thesis: [s,F4()] in F
then for Y being set st Y in M holds
[s,F4()] in Y by A1;
hence [s,F4()] in F by SETFAM_1:def 1; :: thesis: verum
end;
let s be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let a be Element of F1(); :: thesis: for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let v be Element of F3(); :: thesis: ( [s,v] in F implies [(push (a,s)),F5(a,v)] in F )
assume A5: [s,v] in F ; :: thesis: [(push (a,s)),F5(a,v)] in F
now :: thesis: for Y being set st Y in M holds
[(push (a,s)),F5(a,v)] in Y
let Y be set ; :: thesis: ( Y in M implies [(push (a,s)),F5(a,v)] in Y )
assume Y in M ; :: thesis: [(push (a,s)),F5(a,v)] in Y
then ( S1[Y] & [s,v] in Y ) by A5, A1, SETFAM_1:def 1;
hence [(push (a,s)),F5(a,v)] in Y ; :: thesis: verum
end;
hence [(push (a,s)),F5(a,v)] in F by SETFAM_1:def 1; :: thesis: verum
end;
defpred S3[ stack of F1()] means ex y being set st [$1,y] in F;
A6: for s being stack of F1() st emp s holds
S3[s]
proof
let s be stack of F1(); :: thesis: ( emp s implies S3[s] )
assume A7: emp s ; :: thesis: S3[s]
take y = F4(); :: thesis: [s,y] in F
for Y being set st Y in M holds
[s,F4()] in Y by A7, A1;
hence [s,y] in F by SETFAM_1:def 1; :: thesis: verum
end;
A8: for s being stack of F1()
for e being Element of F1() st S3[s] holds
S3[ push (e,s)]
proof
let s be stack of F1(); :: thesis: for e being Element of F1() st S3[s] holds
S3[ push (e,s)]
let e be Element of F1(); :: thesis: ( S3[s] implies S3[ push (e,s)] )
given y being set such that A9: [s,y] in F ; :: thesis: S3[ push (e,s)]
reconsider y = y as Element of F3() by A9, ZFMISC_1:87;
take z = F5(e,y); :: thesis: [(push (e,s)),z] in F
now :: thesis: for Y being set st Y in M holds
[(push (e,s)),z] in Y
let Y be set ; :: thesis: ( Y in M implies [(push (e,s)),z] in Y )
assume A10: Y in M ; :: thesis: [(push (e,s)),z] in Y
then [s,y] in Y by A9, SETFAM_1:def 1;
hence [(push (e,s)),z] in Y by A10, A1; :: thesis: verum
end;
hence [(push (e,s)),z] in F by SETFAM_1:def 1; :: thesis: verum
end;
A11: for s being stack of F1() st emp s holds
S2[s]
proof
let s be stack of F1(); :: thesis: ( emp s implies S2[s] )
assume A12: emp s ; :: thesis: S2[s]
let y1, y2 be object ; :: thesis: ( [s,y1] in F & [s,y2] in F implies y1 = y2 )
assume A13: ( [s,y1] in F & [s,y2] in F ) ; :: thesis: y1 = y2
set Y1 = F \ {[s,y1]};
set Y2 = F \ {[s,y2]};
A14: now :: thesis: not y1 <> F4()
assume A15: y1 <> F4() ; :: thesis: contradiction
S1[F \ {[s,y1]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[s,y1]} holds
[(push (a,s)),F5(a,v)] in F \ {[s,y1]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[s,y1]} )
assume emp s1 ; :: thesis: [s1,F4()] in F \ {[s,y1]}
then A16: [s1,F4()] in F by A4;
[s,y1] <> [s1,F4()] by A15, XTUPLE_0:1;
then [s1,F4()] nin {[s,y1]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[s,y1]} by A16, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[s,y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[s,y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[s,y1]} implies [(push (a,s1)),F5(a,v)] in F \ {[s,y1]} )
assume [s1,v] in F \ {[s,y1]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
then [s1,v] in F by XBOOLE_0:def 5;
then A17: [(push (a,s1)),F5(a,v)] in F by A4;
push (a,s1) <> s by A12, Def12;
then [s,y1] <> [(push (a,s1)),F5(a,v)] by XTUPLE_0:1;
then [(push (a,s1)),F5(a,v)] nin {[s,y1]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[s,y1]} by A17, XBOOLE_0:def 5; :: thesis: verum
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: verum
end;
now :: thesis: not y2 <> F4()
assume A18: y2 <> F4() ; :: thesis: contradiction
S1[F \ {[s,y2]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[s,y2]} holds
[(push (a,s)),F5(a,v)] in F \ {[s,y2]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[s,y2]} )
assume emp s1 ; :: thesis: [s1,F4()] in F \ {[s,y2]}
then A19: [s1,F4()] in F by A4;
[s,y2] <> [s1,F4()] by A18, XTUPLE_0:1;
then [s1,F4()] nin {[s,y2]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[s,y2]} by A19, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[s,y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[s,y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[s,y2]} implies [(push (a,s1)),F5(a,v)] in F \ {[s,y2]} )
assume [s1,v] in F \ {[s,y2]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
then [s1,v] in F by XBOOLE_0:def 5;
then A20: [(push (a,s1)),F5(a,v)] in F by A4;
push (a,s1) <> s by A12, Def12;
then [s,y2] <> [(push (a,s1)),F5(a,v)] by XTUPLE_0:1;
then [(push (a,s1)),F5(a,v)] nin {[s,y2]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[s,y2]} by A20, XBOOLE_0:def 5; :: thesis: verum
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: verum
end;
hence y1 = y2 by A14; :: thesis: verum
end;
A21: for s being stack of F1()
for e being Element of F1() st S2[s] holds
S2[ push (e,s)]
proof
let s be stack of F1(); :: thesis: for e being Element of F1() st S2[s] holds
S2[ push (e,s)]
let e be Element of F1(); :: thesis: ( S2[s] implies S2[ push (e,s)] )
assume A22: S2[s] ; :: thesis: S2[ push (e,s)]
let y1, y2 be object ; :: thesis: ( [(push (e,s)),y1] in F & [(push (e,s)),y2] in F implies y1 = y2 )
assume A23: ( [(push (e,s)),y1] in F & [(push (e,s)),y2] in F ) ; :: thesis: y1 = y2
S3[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 F3() by A24, ZFMISC_1:87;
set Y1 = F \ {[(push (e,s)),y1]};
set Y2 = F \ {[(push (e,s)),y2]};
A25: now :: thesis: not y1 <> F5(e,y)
assume A26: y1 <> F5(e,y) ; :: thesis: contradiction
S1[F \ {[(push (e,s)),y1]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[(push (e,s)),y1]} )
assume A27: emp s1 ; :: thesis: [s1,F4()] in F \ {[(push (e,s)),y1]}
then A28: [s1,F4()] in F by A4;
not emp push (e,s) by Def12;
then [(push (e,s)),y1] <> [s1,F4()] by A27, XTUPLE_0:1;
then [s1,F4()] nin {[(push (e,s)),y1]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[(push (e,s)),y1]} by A28, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[(push (e,s)),y1]} implies [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]} )
assume [s1,v] in F \ {[(push (e,s)),y1]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
then A29: [s1,v] in F by XBOOLE_0:def 5;
then A30: [(push (a,s1)),F5(a,v)] in F by A4;
now :: thesis: not [(push (e,s)),y1] = [(push (a,s1)),F5(a,v)]
assume [(push (e,s)),y1] = [(push (a,s1)),F5(a,v)] ; :: thesis: contradiction
then A31: ( push (e,s) = push (a,s1) & y1 = F5(a,v) ) by XTUPLE_0:1;
then ( e = a & s = s1 ) by Th3;
hence contradiction by A22, A24, A29, A26, A31; :: thesis: verum
end;
then [(push (a,s1)),F5(a,v)] nin {[(push (e,s)),y1]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]} by A30, XBOOLE_0:def 5; :: thesis: verum
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: verum
end;
now :: thesis: not y2 <> F5(e,y)
assume A32: y2 <> F5(e,y) ; :: thesis: contradiction
S1[F \ {[(push (e,s)),y2]}]
proof
hereby :: thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let s1 be stack of F1(); :: thesis: ( emp s1 implies [s1,F4()] in F \ {[(push (e,s)),y2]} )
assume A33: emp s1 ; :: thesis: [s1,F4()] in F \ {[(push (e,s)),y2]}
then A34: [s1,F4()] in F by A4;
not emp push (e,s) by Def12;
then [(push (e,s)),y2] <> [s1,F4()] by A33, XTUPLE_0:1;
then [s1,F4()] nin {[(push (e,s)),y2]} by TARSKI:def 1;
hence [s1,F4()] in F \ {[(push (e,s)),y2]} by A34, XBOOLE_0:def 5; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let a be Element of F1(); :: thesis: for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let v be Element of F3(); :: thesis: ( [s1,v] in F \ {[(push (e,s)),y2]} implies [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]} )
assume [s1,v] in F \ {[(push (e,s)),y2]} ; :: thesis: [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
then A35: [s1,v] in F by XBOOLE_0:def 5;
then A36: [(push (a,s1)),F5(a,v)] in F by A4;
now :: thesis: not [(push (e,s)),y2] = [(push (a,s1)),F5(a,v)]
assume [(push (e,s)),y2] = [(push (a,s1)),F5(a,v)] ; :: thesis: contradiction
then A37: ( push (e,s) = push (a,s1) & y2 = F5(a,v) ) by XTUPLE_0:1;
then ( e = a & s = s1 ) by Th3;
hence contradiction by A22, A24, A35, A32, A37; :: thesis: verum
end;
then [(push (a,s1)),F5(a,v)] nin {[(push (e,s)),y2]} by TARSKI:def 1;
hence [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]} by A36, XBOOLE_0:def 5; :: thesis: verum
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: verum
end;
hence y1 = y2 by A25; :: thesis: verum
end;
A38: F is Function-like
proof
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in F or not [x,y2] in F or y1 = y2 )
assume A39: ( [x,y1] in F & [x,y2] in F ) ; :: thesis: y1 = y2
then reconsider x = x as stack of F1() by ZFMISC_1:87;
S2[x] from STACKS_1:sch 3(A11, A21);
hence y1 = y2 by A39; :: thesis: verum
end;
F is quasi_total
proof
per cases ( F3() <> {} or F3() = {} ) ;
:: according to FUNCT_2:def 1
case F3() <> {} ; :: thesis: the carrier' of F1() = dom F
thus the carrier' of F1() c= dom F :: according to XBOOLE_0:def 10 :: thesis: dom F c= the carrier' of F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of F1() or x in dom F )
assume x in the carrier' of F1() ; :: thesis: x in dom F
then reconsider x = x as stack of F1() ;
S3[x] from STACKS_1:sch 3(A6, A8);
hence x in dom F by XTUPLE_0:def 12; :: thesis: verum
end;
thus dom F c= the carrier' of F1() ; :: thesis: verum
end;
end;
end;
then reconsider F = F as Function of the carrier' of F1(),F3() by A38;
take a = F . F2(); :: thesis: ex F being Function of the carrier' of F1(),F3() st
( a = 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)) ) )
take F ; :: thesis: ( a = 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)) ) )
thus a = F . F2() ; :: thesis: ( ( 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)) ) )
hereby :: thesis: for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1))
let s1 be stack of F1(); :: thesis: ( emp s1 implies F . s1 = F4() )
assume emp s1 ; :: thesis: F . s1 = F4()
then [s1,F4()] in F by A4;
hence F . s1 = F4() by FUNCT_1:1; :: thesis: verum
end;
let s1 be stack of F1(); :: thesis: for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1))
let e be Element of F1(); :: thesis: F . (push (e,s1)) = F5(e,(F . s1))
dom F = the carrier' of F1() by FUNCT_2:def 1;
then [s1,(F . s1)] in F by FUNCT_1:def 2;
then [(push (e,s1)),F5(e,(F . s1))] in F by A4;
hence F . (push (e,s1)) = F5(e,(F . s1)) by FUNCT_1:1; :: thesis: verum