set w = sup the carrier' of J;
deffunc H1( ConnectivesSignature ) -> FinSequence of the carrier' of n = the connectives of n;
defpred S1[ Nat, ConnectivesSignature ] means H1(X) . (n + n) = (sup the carrier' of J) +^ n;
consider S being non empty non void strict AlgLangSignature over X such that
A1: ( S is n PC-correct & S is QC-correct & S is n AL-correct & S is J -extension ) and
A2: for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of S . (n + i) = (sup the carrier' of J) +^ i and
A3: ( ( for x being Element of X holds
( the quantifiers of S . (1,x) = [ the carrier' of J,1,x] & the quantifiers of S . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of S = sup the carrier of J & the program-sort of S = (sup the carrier of J) +^ 1 ) and
( the carrier of S = the carrier of J \/ { the formula-sort of S, the program-sort of S} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of S = ( the carrier' of J \/ {(w +^ 0),(w +^ 1),(w +^ 2),(w +^ 3),(w +^ 4),(w +^ 5),(w +^ 6),(w +^ 7),(w +^ 8)}) \/ [:{ the carrier' of J},{1,2},X:] ) ) by Th11;
reconsider S = S as non empty non void J -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X by A1;
take S ; :: thesis: S is essential
set c = the connectives of S;
thus the connectives of S .: ((n + 9) \ n) misses the carrier' of J :: according to AOFA_L00:def 18 :: thesis: ( rng the quantifiers of S misses the carrier' of J & { the formula-sort of S, the program-sort of S} misses the carrier of J )
proof
assume the connectives of S .: ((n + 9) \ n) meets the carrier' of J ; :: thesis: contradiction
then consider x being object such that
A4: ( x in the connectives of S .: ((n + 9) \ n) & x in the carrier' of J ) by XBOOLE_0:3;
consider k being object such that
A5: ( k in dom the connectives of S & k in (n + 9) \ n & x = the connectives of S . k ) by A4, FUNCT_1:def 6;
reconsider k = k as Nat by A5;
set k1 = k -' n;
A6: ( k in Segm (n + 9) & k nin n ) by A5, XBOOLE_0:def 5;
then Segm n c= Segm k by ORDINAL1:16;
then ( n <= k & k < (n + 8) + 1 ) by A6, NAT_1:44;
then ( n <= k & k <= n + 8 ) by NAT_1:13;
then A7: ( n + 0 <= n + (k -' n) & n + (k -' n) <= n + 8 & k = n + (k -' n) ) by XREAL_1:235;
then ( 0 <= k -' n & k -' n <= 8 ) by XREAL_1:6;
then not not 0 = k -' n & ... & not 8 = k -' n ;
then the connectives of S . k = (sup the carrier' of J) +^ (k -' n) by A2, A7;
then ( (sup the carrier' of J) +^ (k -' n) in sup the carrier' of J & sup the carrier' of J = (sup the carrier' of J) +^ 0 ) by A4, A5, ORDINAL2:19, ORDINAL2:27;
hence contradiction by ORDINAL3:22; :: thesis: verum
end;
thus rng the quantifiers of S misses the carrier' of J :: thesis: { the formula-sort of S, the program-sort of S} misses the carrier of J
proof
assume rng the quantifiers of S meets the carrier' of J ; :: thesis: contradiction
then consider x being object such that
A8: ( x in rng the quantifiers of S & x in the carrier' of J ) by XBOOLE_0:3;
consider y being object such that
A9: ( y in dom the quantifiers of S & x = the quantifiers of S . y ) by A8, FUNCT_1:def 3;
dom the quantifiers of S = [: the quant-sort of S,X:] by FUNCT_2:def 1
.= [:{1,2},X:] by Def5 ;
then consider i, z being object such that
A10: ( i in {1,2} & z in X & y = [i,z] ) by A9, ZFMISC_1:def 2;
( i = 1 or i = 2 ) by A10, TARSKI:def 2;
then ( x = the quantifiers of S . (i,z) & the quantifiers of S . (i,z) = [ the carrier' of J,i,z] ) by A9, A10, A3;
then ( the carrier' of J in { the carrier' of J} & { the carrier' of J} in {{ the carrier' of J,i},{ the carrier' of J}} & {{ the carrier' of J,i},{ the carrier' of J}} in {[ the carrier' of J,i]} & {[ the carrier' of J,i]} in the quantifiers of S . (i,z) & the quantifiers of S . (i,z) = x & x in the carrier' of J ) by A8, TARSKI:def 1, TARSKI:def 2;
hence contradiction by XREGULAR:9; :: thesis: verum
end;
assume { the formula-sort of S, the program-sort of S} meets the carrier of J ; :: thesis: contradiction
then consider x being object such that
A11: ( x in { the formula-sort of S, the program-sort of S} & x in the carrier of J ) by XBOOLE_0:3;
( x = the formula-sort of S or x = the program-sort of S ) by A11, TARSKI:def 2;
then ( sup the carrier of J in sup the carrier of J or (sup the carrier of J) +^ 1 in sup the carrier of J ) by A3, A11, ORDINAL2:19;
then (sup the carrier of J) +^ 1 in (sup the carrier of J) +^ 0 by ORDINAL2:27;
hence contradiction by ORDINAL3:22; :: thesis: verum