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 A1, A2, NAT_1:12, XXREAL_0:2;

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 A4, A3, FUNCT_1:102, SUBSET_1:def 8;

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 A4, A3, FUNCT_1:102, SUBSET_1:def 8;

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 A3, FUNCT_1:102, SUBSET_1:def 8;

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 FUNCT_2:def 1, ZFMISC_1:def 2;

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 SUBSET_1:def 8, FUNCT_1:102;

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 A5, Def5;

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

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 A1, A2, NAT_1:12, XXREAL_0:2;

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 A4, A3, FUNCT_1:102, SUBSET_1:def 8;

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 A4, A3, FUNCT_1:102, SUBSET_1:def 8;

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 A3, FUNCT_1:102, SUBSET_1:def 8;

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 FUNCT_2:def 1, ZFMISC_1:def 2;

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 SUBSET_1:def 8, FUNCT_1:102;

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 A5, Def5;

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