consider Q being non empty non void n PC-correct QC-correct QCLangSignature over X such that
A4: ( the carrier of Q misses the carrier of J & the carrier' of Q misses the carrier' of J ) by Th21;
set C = the carrier of Q \/ the carrier of J;
set C9 = the carrier' of Q \/ the carrier' of J;
A5: ( the carrier' of Q c= the carrier' of Q \/ the carrier' of J & the carrier' of J c= the carrier' of Q \/ the carrier' of J ) by XBOOLE_1:7;
( the carrier of Q * c= ( the carrier of Q \/ the carrier of J) * & the carrier of J * c= ( the carrier of Q \/ the carrier of J) * ) by ;
then A6: ( ( the carrier of Q *) \/ ( the carrier of J *) c= (( the carrier of Q \/ the carrier of J) *) \/ (( the carrier of Q \/ the carrier of J) *) & (( the carrier of Q \/ the carrier of J) *) \/ (( the carrier of Q \/ the carrier of J) *) = ( the carrier of Q \/ the carrier of J) * ) by XBOOLE_1:13;
set A = the Arity of Q +* the Arity of J;
(rng the Arity of Q) \/ (rng the Arity of J) c= ( the carrier of Q *) \/ ( the carrier of J *) by XBOOLE_1:13;
then ( rng ( the Arity of Q +* the Arity of J) c= (rng the Arity of Q) \/ (rng the Arity of J) & (rng the Arity of Q) \/ (rng the Arity of J) c= ( the carrier of Q \/ the carrier of J) * & dom the Arity of Q = the carrier' of Q & dom the Arity of J = the carrier' of J ) by ;
then ( dom ( the Arity of Q +* the Arity of J) = the carrier' of Q \/ the carrier' of J & rng ( the Arity of Q +* the Arity of J) c= ( the carrier of Q \/ the carrier of J) * ) by FUNCT_4:def 1;
then reconsider A = the Arity of Q +* the Arity of J as Function of ( the carrier' of Q \/ the carrier' of J),(( the carrier of Q \/ the carrier of J) *) by FUNCT_2:2;
set R = the ResultSort of Q +* the ResultSort of J;
( rng ( the ResultSort of Q +* the ResultSort of J) c= (rng the ResultSort of Q) \/ (rng the ResultSort of J) & (rng the ResultSort of Q) \/ (rng the ResultSort of J) c= the carrier of Q \/ the carrier of J & dom the ResultSort of Q = the carrier' of Q & dom the ResultSort of J = the carrier' of J ) by ;
then ( dom ( the ResultSort of Q +* the ResultSort of J) = the carrier' of Q \/ the carrier' of J & rng ( the ResultSort of Q +* the ResultSort of J) c= the carrier of Q \/ the carrier of J ) by FUNCT_4:def 1;
then reconsider R = the ResultSort of Q +* the ResultSort of J as Function of ( the carrier' of Q \/ the carrier' of J),( the carrier of Q \/ the carrier of J) by FUNCT_2:2;
reconsider f = the formula-sort of Q as Element of the carrier of Q \/ the carrier of J by XBOOLE_0:def 3;
rng the connectives of Q c= the carrier' of Q \/ the carrier' of J by A5;
then reconsider c = the connectives of Q as FinSequence of the carrier' of Q \/ the carrier' of J by FINSEQ_1:def 4;
rng the quantifiers of Q c= the carrier' of Q \/ the carrier' of J by A5;
then reconsider q = the quantifiers of Q as Function of [: the quant-sort of Q,X:],( the carrier' of Q \/ the carrier' of J) by FUNCT_2:6;
reconsider E = QCLangSignature(# ( the carrier of Q \/ the carrier of J),( the carrier' of Q \/ the carrier' of J),A,R,f,c, the quant-sort of Q,q #) as non empty non void QCLangSignature over X ;
A7: ( Q +* J is Extension of J & J +* Q is Extension of Q ) by ALGSPEC1:48;
set sE = ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #);
( dom the Arity of J = the carrier' of J & dom the Arity of Q = the carrier' of Q & dom the ResultSort of J = the carrier' of J & dom the ResultSort of Q = the carrier' of Q ) by FUNCT_2:def 1;
then ( not ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) is empty & the carrier of ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = the carrier of Q \/ the carrier of J & the carrier' of ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = the carrier' of Q \/ the carrier' of J & the Arity of ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = the Arity of Q +* the Arity of J & the Arity of Q +* the Arity of J = the Arity of J +* the Arity of Q & the ResultSort of ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = the ResultSort of Q +* the ResultSort of J & the ResultSort of Q +* the ResultSort of J = the ResultSort of J +* the ResultSort of Q ) by ;
then ( ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = Q +* J & ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = J +* Q & ManySortedSign(# the carrier of Q, the carrier' of Q, the Arity of Q, the ResultSort of Q #) = ManySortedSign(# the carrier of Q, the carrier' of Q, the Arity of Q, the ResultSort of Q #) & ManySortedSign(# the carrier of J, the carrier' of J, the Arity of J, the ResultSort of J #) = ManySortedSign(# the carrier of J, the carrier' of J, the Arity of J, the ResultSort of J #) ) by CIRCCOMB:def 2;
then A8: ( E is Extension of J & E is Extension of Q ) by ;
A9: E is n PC-correct
proof
A10: ( len the connectives of Q >= n + 5 & the connectives of Q | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one & the connectives of Q . n is_of_type <* the formula-sort of Q*>, the formula-sort of Q & the connectives of Q . (n + 5) is_of_type {} , the formula-sort of Q & the connectives of Q . (n + 1) is_of_type <* the formula-sort of Q, the formula-sort of Q*>, the formula-sort of Q & ... & the connectives of Q . (n + 4) is_of_type <* the formula-sort of Q, the formula-sort of Q*>, the formula-sort of Q ) by Def4;
thus len the connectives of E >= n + 5 by Def4; :: according to AOFA_L00:def 4 :: thesis: ( the connectives of E | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one & the connectives of E . n is_of_type <* the formula-sort of E*>, the formula-sort of E & the connectives of E . (n + 5) is_of_type {} , the formula-sort of E & the connectives of E . (n + 1) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E & ... & the connectives of E . (n + 4) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E )
thus the connectives of E | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one by Def4; :: thesis: ( the connectives of E . n is_of_type <* the formula-sort of E*>, the formula-sort of E & the connectives of E . (n + 5) is_of_type {} , the formula-sort of E & the connectives of E . (n + 1) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E & ... & the connectives of E . (n + 4) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E )
( 0 < n & n <= n + 5 ) by NAT_1:12;
then ( 0 + 1 <= n & n <= len the connectives of Q ) by ;
then n in dom the connectives of Q by FINSEQ_3:25;
then the connectives of E . n is OperSymbol of Q by FUNCT_1:102;
hence the connectives of E . n is_of_type <* the formula-sort of E*>, the formula-sort of E by A10, A8, Th9; :: thesis: ( the connectives of E . (n + 5) is_of_type {} , the formula-sort of E & the connectives of E . (n + 1) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E & ... & the connectives of E . (n + 4) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E )
( 1 <= (n + 4) + 1 & (n + 4) + 1 = n + 5 & n + 5 <= len the connectives of Q ) by ;
then n + 5 in dom the connectives of Q by FINSEQ_3:25;
then the connectives of E . (n + 5) is OperSymbol of Q by FUNCT_1:102;
hence the connectives of E . (n + 5) is_of_type {} , the formula-sort of E by A10, A8, Th9; :: thesis: the connectives of E . (n + 1) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E & ... & the connectives of E . (n + 4) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E
( n + 1 <= (n + 1) + 4 & (n + 1) + 4 = n + 5 & (n + 1) + 1 = n + 2 & n + 2 <= (n + 2) + 3 & (n + 2) + 3 = n + 5 & (n + 2) + 1 = n + 3 & n + 3 <= (n + 3) + 2 & (n + 3) + 2 = n + 5 & (n + 3) + 1 = n + 4 & n + 4 <= (n + 4) + 1 & (n + 4) + 1 = n + 5 ) by NAT_1:12;
then ( 1 <= n + 1 & n + 1 <= len the connectives of Q ) & ... & ( 1 <= n + 4 & n + 4 <= len the connectives of Q ) by ;
then n + 1 in dom the connectives of Q & ... & n + 4 in dom the connectives of Q by FINSEQ_3:25;
then the connectives of E . (n + 1) is OperSymbol of Q & ... & the connectives of E . (n + 4) is OperSymbol of Q by FUNCT_1:102;
hence the connectives of E . (n + 1) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E & ... & the connectives of E . (n + 4) is_of_type <* the formula-sort of E, the formula-sort of E*>, the formula-sort of E by A10, A8, Th9; :: thesis: verum
end;
E is QC-correct
proof
thus ( the quant-sort of E = {1,2} & the quantifiers of E is one-to-one ) by Def5; :: according to AOFA_L00:def 5 :: thesis: ( rng the quantifiers of E misses rng the connectives of E & ( for q, x being object st q in the quant-sort of E & x in X holds
the quantifiers of E . (q,x) is_of_type <* the formula-sort of E*>, the formula-sort of E ) )

thus rng the quantifiers of E misses rng the connectives of E by Def5; :: thesis: for q, x being object st q in the quant-sort of E & x in X holds
the quantifiers of E . (q,x) is_of_type <* the formula-sort of E*>, the formula-sort of E

let q, x be object ; :: thesis: ( q in the quant-sort of E & x in X implies the quantifiers of E . (q,x) is_of_type <* the formula-sort of E*>, the formula-sort of E )
assume A11: ( q in the quant-sort of E & x in X ) ; :: thesis: the quantifiers of E . (q,x) is_of_type <* the formula-sort of E*>, the formula-sort of E
[q,x] in [: the quant-sort of Q,X:] by ;
then ( the quantifiers of E . (q,x) is OperSymbol of Q & the quantifiers of Q . (q,x) is_of_type <* the formula-sort of Q*>, the formula-sort of Q ) by ;
hence the quantifiers of E . (q,x) is_of_type <* the formula-sort of E*>, the formula-sort of E by ; :: thesis: verum
end;
then reconsider E = E as non empty non void n PC-correct QC-correct QCLangSignature over X by A9;
take E ; :: thesis: E is J -extension
thus J is Subsignature of E by ; :: according to AOFA_L00:def 2 :: thesis: verum