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
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;
AOFA_L00:def 4 ( 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;
( 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;
( 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;
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;
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;
AOFA_L00:def 5 ( 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;
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 ;
( 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 )
;
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;
verum
end;
then reconsider E = E as non empty non void n PC-correct QC-correct QCLangSignature over X by A9;
take
E
; E is J -extension
thus
J is Subsignature of E
by A8, ALGSPEC1:def 5; AOFA_L00:def 2 verum