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