let n be natural non empty number ; :: thesis: for X being non empty set
for J being Signature ex S being non empty non void strict AlgLangSignature over X st
( S is n PC-correct & S is QC-correct & S is n AL-correct & S is J -extension & ( 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 ) & ( 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 & 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:] ) )
let X be non empty set ; :: thesis: for J being Signature ex S being non empty non void strict AlgLangSignature over X st
( S is n PC-correct & S is QC-correct & S is n AL-correct & S is J -extension & ( 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 ) & ( 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 & 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:] ) )
let J be Signature; :: thesis: ex S being non empty non void strict AlgLangSignature over X st
( S is n PC-correct & S is QC-correct & S is n AL-correct & S is J -extension & ( 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 ) & ( 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 & 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:] ) )
set w = sup the carrier' of J;
set u = sup the carrier of J;
set O1 = {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:];
set O = the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]);
set a = ((({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 0)*>) \/ (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*((sup the carrier of J) +^ 0)*>)) \/ ({((sup the carrier' of J) +^ 5)} --> {})) \/ ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*((sup the carrier of J) +^ 1),((sup the carrier of J) +^ 0)*>);
set ay = the Arity of J \/ (((({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 0)*>) \/ (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*((sup the carrier of J) +^ 0)*>)) \/ ({((sup the carrier' of J) +^ 5)} --> {})) \/ ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*((sup the carrier of J) +^ 1),((sup the carrier of J) +^ 0)*>));
set r = ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0);
set rs = the ResultSort of J +* (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0));
A1: ( dom ({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 0)*>) = {((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} & dom ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*((sup the carrier of J) +^ 1),((sup the carrier of J) +^ 0)*>) = {((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} & dom ({((sup the carrier' of J) +^ 5)} --> {}) = {((sup the carrier' of J) +^ 5)} & dom (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*((sup the carrier of J) +^ 0)*>) = {((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:] ) ;
B1: {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} misses [:{ the carrier' of J},{1,2},X:] {((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} misses {((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:] then reconsider aa = ({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 0)*>) \/ (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*((sup the carrier of J) +^ 0)*>) as Function by A1, GRFUNC_1:13;
A6: dom aa = {((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} \/ ({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) by A1, XTUPLE_0:23
.= ({((sup the carrier' of J) +^ 0)} \/ {((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)}) \/ [:{ the carrier' of J},{1,2},X:] by XBOOLE_1:4
.= {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} \/ [:{ the carrier' of J},{1,2},X:] by ENUMSET1:7 ;
{((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} \/ [:{ the carrier' of J},{1,2},X:] misses {((sup the carrier' of J) +^ 5)} then reconsider ab = aa \/ ({((sup the carrier' of J) +^ 5)} --> {}) as Function by A1, A6, GRFUNC_1:13;
A9: dom ab = ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} \/ [:{ the carrier' of J},{1,2},X:]) \/ {((sup the carrier' of J) +^ 5)} by A1, A6, XTUPLE_0:23
.= ({((sup the carrier' of J) +^ 5)} \/ {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)}) \/ [:{ the carrier' of J},{1,2},X:] by XBOOLE_1:4
.= {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5)} \/ [:{ the carrier' of J},{1,2},X:] by ENUMSET1:15 ;
{((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5)} \/ [:{ the carrier' of J},{1,2},X:] misses {((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} then reconsider a = ((({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 0)*>) \/ (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*((sup the carrier of J) +^ 0)*>)) \/ ({((sup the carrier' of J) +^ 5)} --> {})) \/ ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*((sup the carrier of J) +^ 1),((sup the carrier of J) +^ 0)*>) as Function by A1, A9, GRFUNC_1:13;
A14: dom a = ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5)} \/ [:{ the carrier' of J},{1,2},X:]) \/ {((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} by A1, A9, XTUPLE_0:23
.= ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5)}) \/ [:{ the carrier' of J},{1,2},X:] by XBOOLE_1:4
.= {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:] by ENUMSET1:82 ;
then A15: ( dom ( the Arity of J \/ (((({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 0)*>) \/ (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*((sup the carrier of J) +^ 0)*>)) \/ ({((sup the carrier' of J) +^ 5)} --> {})) \/ ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*((sup the carrier of J) +^ 1),((sup the carrier of J) +^ 0)*>))) = (dom the Arity of J) \/ (dom a) & (dom the Arity of J) \/ (dom a) = the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) ) by XTUPLE_0:23, FUNCT_2:def 1;
A16: dom the Arity of J = the carrier' of J by FUNCT_2:def 1;
A17: {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:] misses the carrier' of J then reconsider ay = the Arity of J \/ a as Function by A14, A16, GRFUNC_1:13;
set C = the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)};
( (sup the carrier of J) +^ 0 in {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} & (sup the carrier of J) +^ 1 in {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} ) by TARSKI:def 2;
then reconsider 00 = (sup the carrier of J) +^ 0, 01 = (sup the carrier of J) +^ 1 as Element of the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} by XBOOLE_0:def 3;
( <*00*> in ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * & <*00,00*> in ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by FINSEQ_1:def 11;
then ( rng ({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*00,00*>) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * & rng (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*00*>) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by ZFMISC_1:31;
then ( (rng ({((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} --> <*00,00*>)) \/ (rng (({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*00*>)) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * & <*> ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) in ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by FINSEQ_1:def 11, XBOOLE_1:8;
then ( rng aa c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * & rng ({((sup the carrier' of J) +^ 5)} --> {}) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by RELAT_1:12;
then ( (rng aa) \/ (rng ({((sup the carrier' of J) +^ 5)} --> {})) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * & <*01,00*> in ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by FINSEQ_1:def 11, XBOOLE_1:8;
then ( rng ab c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * & rng ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*01,00*>) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by ZFMISC_1:31, RELAT_1:12;
then (rng ab) \/ (rng ({((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*01,00*>)) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * by XBOOLE_1:8;
then A20: rng a c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * by RELAT_1:12;
( rng the Arity of J c= the carrier of J * & the carrier of J * c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by XBOOLE_1:7, FINSEQ_1:62;
then rng the Arity of J c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ;
then ( rng ay = (rng the Arity of J) \/ (rng a) & (rng the Arity of J) \/ (rng a) c= ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) * ) by A20, XBOOLE_1:8, RELAT_1:12;
then reconsider ay = ay as Function of ( the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:])),(( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) *) by A15, FUNCT_2:2;
( the carrier' of J <> {} implies the carrier of J <> {} ) by INSTALG1:def 1;
then A21: ( dom (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0)) = {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:] & rng (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0)) = {00} & {00} c= the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} & dom the ResultSort of J = the carrier' of J & rng the ResultSort of J c= the carrier of J & the carrier of J c= the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} ) by XBOOLE_1:7, ZFMISC_1:31, FUNCT_2:def 1;
then rng the ResultSort of J c= the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} ;
then ( dom ( the ResultSort of J +* (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0))) = the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) & rng ( the ResultSort of J +* (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0))) c= {00} \/ (rng the ResultSort of J) & {00} \/ (rng the ResultSort of J) c= the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} ) by A21, XBOOLE_1:8, FUNCT_4:def 1, FUNCT_4:17;
then ( dom ( the ResultSort of J +* (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0))) = the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) & rng ( the ResultSort of J +* (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0))) c= the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)} ) ;
then reconsider rs = the ResultSort of J +* (({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) --> ((sup the carrier of J) +^ 0)) as Function of ( the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:])),( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}) by FUNCT_2:2;
(sup the carrier' of J) +^ 0 in {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} & ... & (sup the carrier' of J) +^ 8 in {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} by ENUMSET1:def 7;
then (sup the carrier' of J) +^ 0 in {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:] & ... & (sup the carrier' of J) +^ 8 in {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:] by XBOOLE_0:def 3;
then reconsider o0 = (sup the carrier' of J) +^ 0, o1 = (sup the carrier' of J) +^ 1, o2 = (sup the carrier' of J) +^ 2, o3 = (sup the carrier' of J) +^ 3, o4 = (sup the carrier' of J) +^ 4, o5 = (sup the carrier' of J) +^ 5, o6 = (sup the carrier' of J) +^ 6, o7 = (sup the carrier' of J) +^ 7, o8 = (sup the carrier' of J) +^ 8 as Element of the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) by XBOOLE_0:def 3;
set p = the n -' 1 -element FinSequence of {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)};
B2: ( rng the n -' 1 -element FinSequence of {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} c= {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} & {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} c= {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:] & {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:] c= the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) ) by XBOOLE_1:7;
then ( rng the n -' 1 -element FinSequence of {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} c= {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} & {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} c= the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) ) ;
then reconsider p = the n -' 1 -element FinSequence of {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} as FinSequence of the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) by XBOOLE_1:1, FINSEQ_1:def 4;
set c9 = <*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>;
n > 0 ;
then A22: n >= 0 + 1 by NAT_1:13;
reconsider c = p ^ (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>) as FinSequence of the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) ;
rng (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>) = {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} by AOFA_A00:26;
then B3: ( rng c = (rng p) \/ (rng (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>)) & (rng p) \/ (rng (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>)) c= {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ {((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} ) by B2, XBOOLE_1:13, FINSEQ_1:31;
A23: for i being natural number st not not i = 0 & ... & not i = 8 holds
c . (n + i) = (sup the carrier' of J) +^ i deffunc H₁( object ) -> object = [ the carrier' of J,($1 `1),($1 `2)];
consider q being Function such that
A25: ( dom q = [:{1,2},X:] & ( for x being object st x in [:{1,2},X:] holds
q . x = H₁(x) ) ) from FUNCT_1:sch 3();
rng q c= the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:]) then reconsider q = q as Function of [:{1,2},X:],( the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:])) by A25, FUNCT_2:2;
set L = AlgLangSignature(# ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}),( the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:])),ay,rs,00,01,c,{1,2},q #);
reconsider L = AlgLangSignature(# ( the carrier of J \/ {((sup the carrier of J) +^ 0),((sup the carrier of J) +^ 1)}),( the carrier' of J \/ ({((sup the carrier' of J) +^ 0),((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4),((sup the carrier' of J) +^ 5),((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} \/ [:{ the carrier' of J},{1,2},X:])),ay,rs,00,01,c,{1,2},q #) as non empty non void strict AlgLangSignature over X ;
take L ; :: thesis: ( L is n PC-correct & L is QC-correct & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
( len (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>) = 8 + 1 & len p = n -' 1 & n is Real & 1 is Real ) by CARD_1:def 7;
then A28: ( (len p) + (len (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>)) = ((n -' 1) + 1) + 8 & ((n -' 1) + 1) + 8 = n + 8 ) by A22, XREAL_1:235;
then ( len the connectives of L = n + 8 & n + 8 = (n + 5) + 3 ) by FINSEQ_1:22;
hence len the connectives of L >= n + 5 by NAT_1:12; :: according to AOFA_L00:def 4 :: thesis: ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one & the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L & the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
set N = {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)};
thus the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one :: thesis: ( the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L & the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) ) thus the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L :: thesis: ( the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) ) thus the connectives of L . (n + 5) is_of_type {} , the formula-sort of L :: thesis: ( the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) ) thus the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L :: thesis: ( L is QC-correct & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) ) thus the quant-sort of L = {1,2} ; :: according to AOFA_L00:def 5 :: thesis: ( the quantifiers of L is one-to-one & rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
thus the quantifiers of L is one-to-one :: thesis: ( rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) ) rng the quantifiers of L c= [:{ the carrier' of J},{1,2},X:] hence rng the quantifiers of L misses rng the connectives of L by B1, B3, XBOOLE_1:64; :: thesis: ( ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) & L is n AL-correct & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
thus the program-sort of L <> the formula-sort of L by ORDINAL3:21; :: according to AOFA_L00:def 6 :: thesis: ( len the connectives of L >= n + 8 & the connectives of L . (n + 6) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 8) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
thus len the connectives of L >= n + 8 by A28, FINSEQ_1:22; :: thesis: ( the connectives of L . (n + 6) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 8) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L & L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
thus the connectives of L . (n + 6) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 8) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L :: thesis: ( L is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) ) thus L is J -extension :: thesis: ( ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) ) thus for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of L . (n + i) = (sup the carrier' of J) +^ i by A23; :: thesis: ( ( for x being Element of X holds
( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 & the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
thus ( the formula-sort of L = sup the carrier of J & the program-sort of L = (sup the carrier of J) +^ 1 ) by ORDINAL2:27; :: thesis: ( the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:] ) )
thus the carrier of L = the carrier of J \/ { the formula-sort of L, the program-sort of L} ; :: thesis: for w being Ordinal st w = sup the carrier' of J holds
the carrier' of L = ( 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:]
let w be Ordinal; :: thesis: ( w = sup the carrier' of J implies the carrier' of L = ( 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:] )
assume w = sup the carrier' of J ; :: thesis: the carrier' of L = ( 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:]
hence the carrier' of L = ( 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 XBOOLE_1:4; :: thesis: verum