set Q = the non empty non void QCLangSignature over X;
set C = the carrier of the non empty non void QCLangSignature over X \/ the carrier of J;
set C9 = the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J;
A1: ( the carrier' of the non empty non void QCLangSignature over X c= the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J & the carrier' of J c= the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J ) by XBOOLE_1:7;
( the carrier of the non empty non void QCLangSignature over X * c= ( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) * & the carrier of J * c= ( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) * ) by XBOOLE_1:7, FINSEQ_1:62;
then A2: ( ( the carrier of the non empty non void QCLangSignature over X *) \/ ( the carrier of J *) c= (( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) *) \/ (( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) *) & (( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) *) \/ (( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) *) = ( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) * ) by XBOOLE_1:13;
set A = the Arity of the non empty non void QCLangSignature over X +* the Arity of J;
(rng the Arity of the non empty non void QCLangSignature over X) \/ (rng the Arity of J) c= ( the carrier of the non empty non void QCLangSignature over X *) \/ ( the carrier of J *) by XBOOLE_1:13;
then ( rng ( the Arity of the non empty non void QCLangSignature over X +* the Arity of J) c= (rng the Arity of the non empty non void QCLangSignature over X) \/ (rng the Arity of J) & (rng the Arity of the non empty non void QCLangSignature over X) \/ (rng the Arity of J) c= ( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) * & dom the Arity of the non empty non void QCLangSignature over X = the carrier' of the non empty non void QCLangSignature over X & dom the Arity of J = the carrier' of J ) by A2, FUNCT_4:17, FUNCT_2:def 1;
then ( dom ( the Arity of the non empty non void QCLangSignature over X +* the Arity of J) = the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J & rng ( the Arity of the non empty non void QCLangSignature over X +* the Arity of J) c= ( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) * ) by FUNCT_4:def 1;
then reconsider A = the Arity of the non empty non void QCLangSignature over X +* the Arity of J as Function of ( the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J),(( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) *) by FUNCT_2:2;
set R = the ResultSort of the non empty non void QCLangSignature over X +* the ResultSort of J;
( rng ( the ResultSort of the non empty non void QCLangSignature over X +* the ResultSort of J) c= (rng the ResultSort of the non empty non void QCLangSignature over X) \/ (rng the ResultSort of J) & (rng the ResultSort of the non empty non void QCLangSignature over X) \/ (rng the ResultSort of J) c= the carrier of the non empty non void QCLangSignature over X \/ the carrier of J & dom the ResultSort of the non empty non void QCLangSignature over X = the carrier' of the non empty non void QCLangSignature over X & 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 the non empty non void QCLangSignature over X +* the ResultSort of J) = the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J & rng ( the ResultSort of the non empty non void QCLangSignature over X +* the ResultSort of J) c= the carrier of the non empty non void QCLangSignature over X \/ the carrier of J ) by FUNCT_4:def 1;
then reconsider R = the ResultSort of the non empty non void QCLangSignature over X +* the ResultSort of J as Function of ( the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J),( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J) by FUNCT_2:2;
reconsider f = the formula-sort of the non empty non void QCLangSignature over X as Element of the carrier of the non empty non void QCLangSignature over X \/ the carrier of J by XBOOLE_0:def 3;
rng the connectives of the non empty non void QCLangSignature over X c= the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J by A1;
then reconsider c = the connectives of the non empty non void QCLangSignature over X as FinSequence of the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J by FINSEQ_1:def 4;
rng the quantifiers of the non empty non void QCLangSignature over X c= the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J by A1;
then reconsider q = the quantifiers of the non empty non void QCLangSignature over X as Function of [: the quant-sort of the non empty non void QCLangSignature over X,X:],( the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J) by FUNCT_2:6;
reconsider E = QCLangSignature(# ( the carrier of the non empty non void QCLangSignature over X \/ the carrier of J),( the carrier' of the non empty non void QCLangSignature over X \/ the carrier' of J),A,R,f,c, the quant-sort of the non empty non void QCLangSignature over X,q #) as non empty non void QCLangSignature over X ;
take E ; :: thesis: E is J -extension
A3: the non empty non void QCLangSignature over X +* J is Extension of J by ALGSPEC1:48;
set sE = ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #);
( 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 the non empty non void QCLangSignature over X \/ 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 the non empty non void QCLangSignature over X \/ 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 the non empty non void QCLangSignature over X +* the Arity of J & the ResultSort of ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = the ResultSort of the non empty non void QCLangSignature over X +* the ResultSort of J ) ;
then ( ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) = the non empty non void QCLangSignature over X +* J & 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 E is Extension of J by A3, Th20;
hence J is Subsignature of E by ALGSPEC1:def 5; :: according to AOFA_L00:def 2 :: thesis: verum