set Y = { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } ;
reconsider X = (SepQuadruples F2()) /\ { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } as Subset of [:(CQC-WFF F1()),(QC-symbols F1()),(Fin (bound_QC-variables F1())),(Funcs ((bound_QC-variables F1()),(bound_QC-variables F1()))):] ;
A5: SepQuadruples F2() is_Sep-closed_on F2() by Def13;
X is_Sep-closed_on F2()
proof
A6: [F2(),(index F2()),({}. (bound_QC-variables F1())),(id (bound_QC-variables F1()))] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } by A1;
[F2(),(index F2()),({}. (bound_QC-variables F1())),(id (bound_QC-variables F1()))] in SepQuadruples F2() by Th30;
hence [F2(),(index F2()),({}. (bound_QC-variables F1())),(id (bound_QC-variables F1()))] in X by A6, XBOOLE_0:def 4; :: according to CQC_SIM1:def 12 :: thesis: ( ( for q being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) )
thus for q being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X :: thesis: ( ( for q, r being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) )
proof
let q be Element of CQC-WFF F1(); :: thesis: for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X
let t be QC-symbol of F1(); :: thesis: for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X
let K be Element of Fin (bound_QC-variables F1()); :: thesis: for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X
let f be Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())); :: thesis: ( [('not' q),t,K,f] in X implies [q,t,K,f] in X )
assume A7: [('not' q),t,K,f] in X ; :: thesis: [q,t,K,f] in X
then A8: [('not' q),t,K,f] in SepQuadruples F2() by XBOOLE_0:def 4;
[('not' q),t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } by A7, XBOOLE_0:def 4;
then consider p being Element of CQC-WFF F1(), L being Element of Fin (bound_QC-variables F1()), u being QC-symbol of F1(), h being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) such that
A9: [('not' q),t,K,f] = [p,u,L,h] and
A10: P1[p,u,L,h] ;
A11: t = u by A9, XTUPLE_0:5;
A12: f = h by A9, XTUPLE_0:5;
A13: K = L by A9, XTUPLE_0:5;
'not' q = p by A9, XTUPLE_0:5;
then P1[q,t,K,f] by A2, A8, A10, A11, A13, A12;
then A14: [q,t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } ;
[q,t,K,f] in SepQuadruples F2() by A5, A8;
hence [q,t,K,f] in X by A14, XBOOLE_0:def 4; :: thesis: verum
end;
thus for q, r being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) :: thesis: for q being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
proof
let q, r be Element of CQC-WFF F1(); :: thesis: for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )
let t be QC-symbol of F1(); :: thesis: for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )
let K be Element of Fin (bound_QC-variables F1()); :: thesis: for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )
let f be Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())); :: thesis: ( [(q '&' r),t,K,f] in X implies ( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) )
assume A15: [(q '&' r),t,K,f] in X ; :: thesis: ( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )
then A16: [(q '&' r),t,K,f] in SepQuadruples F2() by XBOOLE_0:def 4;
then A17: [r,(t + (QuantNbr q)),K,f] in SepQuadruples F2() by A5;
[(q '&' r),t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } by A15, XBOOLE_0:def 4;
then consider p being Element of CQC-WFF F1(), L being Element of Fin (bound_QC-variables F1()), u being QC-symbol of F1(), h being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) such that
A18: [(q '&' r),t,K,f] = [p,u,L,h] and
A19: P1[p,u,L,h] ;
A20: t = u by A18, XTUPLE_0:5;
A21: f = h by A18, XTUPLE_0:5;
A22: K = L by A18, XTUPLE_0:5;
A23: q '&' r = p by A18, XTUPLE_0:5;
then P1[q,t,K,f] by A3, A16, A19, A20, A22, A21;
then A24: [q,t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } ;
P1[r,t + (QuantNbr q),K,f] by A3, A16, A19, A23, A20, A22, A21;
then A25: [r,(t + (QuantNbr q)),K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } ;
[q,t,K,f] in SepQuadruples F2() by A5, A16;
hence ( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) by A24, A25, A17, XBOOLE_0:def 4; :: thesis: verum
end;
let q be Element of CQC-WFF F1(); :: thesis: for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
let x be bound_QC-variable of F1(); :: thesis: for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
let t be QC-symbol of F1(); :: thesis: for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
let K be Element of Fin (bound_QC-variables F1()); :: thesis: for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
let f be Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())); :: thesis: ( [(All (x,q)),t,K,f] in X implies [q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X )
assume A26: [(All (x,q)),t,K,f] in X ; :: thesis: [q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
then A27: [(All (x,q)),t,K,f] in SepQuadruples F2() by XBOOLE_0:def 4;
f +* (x .--> (x. t)) is Function of (bound_QC-variables F1()),(bound_QC-variables F1()) by Lm1;
then reconsider g = f +* (x .--> (x. t)) as Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) by FUNCT_2:8;
[(All (x,q)),t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } by A26, XBOOLE_0:def 4;
then consider p being Element of CQC-WFF F1(), L being Element of Fin (bound_QC-variables F1()), u being QC-symbol of F1(), h being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) such that
A28: [(All (x,q)),t,K,f] = [p,u,L,h] and
A29: P1[p,u,L,h] ;
A30: t = u by A28, XTUPLE_0:5;
A31: f = h by A28, XTUPLE_0:5;
A32: K = L by A28, XTUPLE_0:5;
All (x,q) = p by A28, XTUPLE_0:5;
then P1[q,t ++ ,K \/ {x},g] by A4, A27, A29, A30, A32, A31;
then A33: [q,(t ++),(K \/ {.x.}),(f +* (x .--> (x. t)))] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } ;
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in SepQuadruples F2() by A5, A27;
hence [q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X by A33, XBOOLE_0:def 4; :: thesis: verum
end;
then A34: SepQuadruples F2() c= X by Def13;
let q be Element of CQC-WFF F1(); :: thesis: for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds
P1[q,t,K,f]
let t be QC-symbol of F1(); :: thesis: for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds
P1[q,t,K,f]
let K be Element of Fin (bound_QC-variables F1()); :: thesis: for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds
P1[q,t,K,f]
let f be Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())); :: thesis: ( [q,t,K,f] in SepQuadruples F2() implies P1[q,t,K,f] )
assume [q,t,K,f] in SepQuadruples F2() ; :: thesis: P1[q,t,K,f]
then [q,t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } by A34, XBOOLE_0:def 4;
then consider p being Element of CQC-WFF F1(), L being Element of Fin (bound_QC-variables F1()), u being QC-symbol of F1(), h being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) such that
A35: [q,t,K,f] = [p,u,L,h] and
A36: P1[p,u,L,h] ;
A37: t = u by A35, XTUPLE_0:5;
A38: K = L by A35, XTUPLE_0:5;
q = p by A35, XTUPLE_0:5;
hence P1[q,t,K,f] by A35, A36, A37, A38, XTUPLE_0:5; :: thesis: verum