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
; 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; AOFA_L00:def 2 verum