let n be natural non empty number ; :: thesis: for X being non empty set
for S being non empty non void n PC-correct QC-correct QCLangSignature over X
for Q being language MSAlgebra over S holds
( {} in Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),Q) & ( for A being Formula of Q holds
( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) ) ) )

let X be non empty set ; :: thesis: for S being non empty non void n PC-correct QC-correct QCLangSignature over X
for Q being language MSAlgebra over S holds
( {} in Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),Q) & ( for A being Formula of Q holds
( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) ) ) )

let S be non empty non void n PC-correct QC-correct QCLangSignature over X; :: thesis: for Q being language MSAlgebra over S holds
( {} in Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),Q) & ( for A being Formula of Q holds
( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) ) ) )

let Q be language MSAlgebra over S; :: thesis: ( {} in Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),Q) & ( for A being Formula of Q holds
( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) ) ) )

set f = the formula-sort of S;
A1: len the connectives of S >= n + 5 by Def4;
n > 0 ;
then A2: n >= 0 + 1 by NAT_1:13;
n + 0 <= n + 5 & ... & n + 4 <= n + 5 by XREAL_1:6;
then ( 1 <= n + 0 & ... & 1 <= n + 5 & n + 0 <= len the connectives of S & ... & n + 5 <= len the connectives of S ) by ;
then A3: n + 0 in dom the connectives of S & ... & n + 5 in dom the connectives of S by FINSEQ_3:25;
A4: ( the connectives of S . (n + 0) is_of_type <* the formula-sort of S*>, the formula-sort of S & the connectives of S . (n + 1) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & ... & the connectives of S . (n + 4) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & the connectives of S . (n + 5) is_of_type {} , the formula-sort of S ) by Def4;
In (( the connectives of S . (n + 5)), the carrier' of S) is_of_type {} , the formula-sort of S by ;
hence {} in Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),Q) by Th4; :: thesis: for A being Formula of Q holds
( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) )

let A be Formula of Q; :: thesis: ( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) )

In (( the connectives of S . (n + 0)), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S by ;
hence <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) by Th5; :: thesis: for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) )

let B be Formula of Q; :: thesis: ( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) )

In (( the connectives of S . (n + 1)), the carrier' of S) = the connectives of S . (n + 1) & ... & In (( the connectives of S . (n + 4)), the carrier' of S) = the connectives of S . (n + 4) by ;
then In (( the connectives of S . (n + 1)), the carrier' of S) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & ... & In (( the connectives of S . (n + 4)), the carrier' of S) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S by Def4;
hence <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) by Th6; :: thesis: for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) )

let x be Element of X; :: thesis: ( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) )
the quant-sort of S = {1,2} by Def5;
then A5: ( 1 in the quant-sort of S & 2 in the quant-sort of S ) by TARSKI:def 2;
then ( [1,x] in [: the quant-sort of S,X:] & dom the quantifiers of S = [: the quant-sort of S,X:] & [2,x] in [: the quant-sort of S,X:] ) by ;
then ( In (( the quantifiers of S . (1,x)), the carrier' of S) = the quantifiers of S . (1,x) & In (( the quantifiers of S . (2,x)), the carrier' of S) = the quantifiers of S . (2,x) ) by ;
then ( In (( the quantifiers of S . (1,x)), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S & In (( the quantifiers of S . (2,x)), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S ) by ;
hence ( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) by Th5; :: thesis: verum