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 XBOOLE_1:7, FINSEQ_1:62;

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 A6, FUNCT_4:17, FUNCT_2:def 1;

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 XBOOLE_1:13, FUNCT_4:17, FUNCT_2:def 1;

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 A4, FUNCT_4:35;

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 A7, Th20;

A9: E is n PC-correct

take E ; :: thesis: E is J -extension

thus J is Subsignature of E by A8, ALGSPEC1:def 5; :: according to AOFA_L00:def 2 :: thesis: verum

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 XBOOLE_1:7, FINSEQ_1:62;

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 A6, FUNCT_4:17, FUNCT_2:def 1;

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 XBOOLE_1:13, FUNCT_4:17, FUNCT_2:def 1;

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 A4, FUNCT_4:35;

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 A7, Th20;

A9: E is n PC-correct

proof

E is QC-correct
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 A10, XXREAL_0:2, NAT_1:13;

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 Def4, NAT_1:12;

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

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;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 A10, XXREAL_0:2, NAT_1:13;

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 Def4, NAT_1:12;

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

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

proof

then reconsider E = E as non empty non void n PC-correct QC-correct QCLangSignature over X by A9;
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 A11, ZFMISC_1:87;

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 Def5, A11, FUNCT_2:5;

hence the quantifiers of E . (q,x) is_of_type <* the formula-sort of E*>, the formula-sort of E by A8, Th9; :: thesis: verum

end;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 A11, ZFMISC_1:87;

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 Def5, A11, FUNCT_2:5;

hence the quantifiers of E . (q,x) is_of_type <* the formula-sort of E*>, the formula-sort of E by A8, Th9; :: thesis: verum

take E ; :: thesis: E is J -extension

thus J is Subsignature of E by A8, ALGSPEC1:def 5; :: according to AOFA_L00:def 2 :: thesis: verum