let n be natural non empty number ; :: thesis:
let X be set ; :: thesis:
let J be non empty Signature; :: thesis:
set Q = the non empty non void n PC-correct QC-correct QCLangSignature over X;
reconsider A = [: the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X,{ the carrier of J}:] as non empty set ;
reconsider B = [: the carrier' of the non empty non void n PC-correct QC-correct QCLangSignature over X,{ the carrier' of J}:] as non empty set ;
reconsider f = pr1 ( the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X,{ the carrier of J}) as Function of A, the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X ;
reconsider g = pr1 ( the carrier' of the non empty non void n PC-correct QC-correct QCLangSignature over X,{ the carrier' of J}) as Function of B, the carrier' of the non empty non void n PC-correct QC-correct QCLangSignature over X ;
( f is one-to-one & rng f = the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X ) by FUNCT_3:44;
then reconsider f1 = f " as Function of the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X,A by FUNCT_2:25;
A1: ( g is one-to-one & rng g = the carrier' of the non empty non void n PC-correct QC-correct QCLangSignature over X ) by FUNCT_3:44;
then reconsider g1 = g " as Function of the carrier' of the non empty non void n PC-correct QC-correct QCLangSignature over X,B by FUNCT_2:25;
deffunc H₁( object ) -> set = f1 * (In ($1,( the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X *)));
consider ff being Function such that
A2: ( dom ff = the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X * & ( for p being object st p in the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X * holds
ff . p = H₁(p) ) ) from FUNCT_1:sch 3();
rng ff c= A *

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng ff ; :: thesis:
then consider b being object such that
A3: ( b in dom ff & a = ff . b ) by FUNCT_1:def 3;
A4: a = H₁(b) by A2, A3;
( H₁(b) is FinSequence & rng H₁(b) c= A ) ;
then H₁(b) is FinSequence of A by FINSEQ_1:def 4;
hence a in A * by A4, FINSEQ_1:def 11; :: thesis:

end;

then reconsider ff = ff as Function of ( the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X *),(A *) by A2, FUNCT_2:2;
reconsider Ar = (ff * the Arity of the non empty non void n PC-correct QC-correct QCLangSignature over X) * g as Function of B,(A *) ;
reconsider re = (f1 * the ResultSort of the non empty non void n PC-correct QC-correct QCLangSignature over X) * g as Function of B,A ;
A5: ( the formula-sort of the non empty non void n PC-correct QC-correct QCLangSignature over X in the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X & the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X = dom f1 ) by FUNCT_2:def 1;
then reconsider fs = f1 . the formula-sort of the non empty non void n PC-correct QC-correct QCLangSignature over X as Element of A by FUNCT_1:102;
rng (g1 * the connectives of the non empty non void n PC-correct QC-correct QCLangSignature over X) c= B ;
then reconsider co = g1 * the connectives of the non empty non void n PC-correct QC-correct QCLangSignature over X as FinSequence of B by FINSEQ_1:def 4;
reconsider qu = g1 * the quantifiers of the non empty non void n PC-correct QC-correct QCLangSignature over X as Function of [: the quant-sort of the non empty non void n PC-correct QC-correct QCLangSignature over X,X:],B ;
set QQ = QCLangSignature(# A,B,Ar,re,fs,co, the quant-sort of the non empty non void n PC-correct QC-correct QCLangSignature over X,qu #);
A6: QCLangSignature(# A,B,Ar,re,fs,co, the quant-sort of the non empty non void n PC-correct QC-correct QCLangSignature over X,qu #) is n PC-correct

proof

end;

QCLangSignature(# A,B,Ar,re,fs,co, the quant-sort of the non empty non void n PC-correct QC-correct QCLangSignature over X,qu #) is QC-correct

proof

end;

then reconsider QQ = QCLangSignature(# A,B,Ar,re,fs,co, the quant-sort of the non empty non void n PC-correct QC-correct QCLangSignature over X,qu #) as non empty non void n PC-correct QC-correct QCLangSignature over X by A6;
take QQ ; :: thesis:
thus the carrier of QQ misses the carrier of J :: thesis:

proof

assume the carrier of QQ meets the carrier of J ; :: thesis:
then consider a being object such that
A22: ( a in the carrier of QQ & a in the carrier of J ) by XBOOLE_0:3;
consider b, c being object such that
A23: ( b in the carrier of the non empty non void n PC-correct QC-correct QCLangSignature over X & c in { the carrier of J} & a = [b,c] ) by A22, ZFMISC_1:def 2;
reconsider c = c as set by TARSKI:1;
( c in {b,c} & {b,c} in {{b,c},{b}} & {{b,c},{b}} in c ) by A22, A23, TARSKI:def 1, TARSKI:def 2;
hence contradiction by XREGULAR:7; :: thesis:

end;

thus the carrier' of QQ misses the carrier' of J :: thesis:

proof

assume the carrier' of QQ meets the carrier' of J ; :: thesis:
then consider a being object such that
A24: ( a in the carrier' of QQ & a in the carrier' of J ) by XBOOLE_0:3;
consider b, c being object such that
A25: ( b in the carrier' of the non empty non void n PC-correct QC-correct QCLangSignature over X & c in { the carrier' of J} & a = [b,c] ) by A24, ZFMISC_1:def 2;
reconsider c = c as set by TARSKI:1;
( c in {b,c} & {b,c} in {{b,c},{b}} & {{b,c},{b}} in c ) by A24, A25, TARSKI:def 1, TARSKI:def 2;
hence contradiction by XREGULAR:7; :: thesis:

end;