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:]
proof
assume {((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)} meets [:{ the carrier' of J},{1,2},X:] ; :: thesis: contradiction
then consider x being object such that
A2: ( x 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)} & x in [:{ the carrier' of J},{1,2},X:] ) by XBOOLE_0:3;
A3: ( x = (sup the carrier' of J) +^ 0 or x = (sup the carrier' of J) +^ 1 or x = (sup the carrier' of J) +^ 2 or x = (sup the carrier' of J) +^ 3 or x = (sup the carrier' of J) +^ 4 or x = (sup the carrier' of J) +^ 5 or x = (sup the carrier' of J) +^ 6 or x = (sup the carrier' of J) +^ 7 or x = (sup the carrier' of J) +^ 8 ) by ;
consider j, y, z being object such that
A5: ( j in { the carrier' of J} & y in {1,2} & z in X & x = [j,y,z] ) by ;
thus contradiction by A3, A5; :: thesis: verum
end;
{((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:]
proof
assume {((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} meets {((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:] ; :: thesis: contradiction
then consider x being object such that
A2: ( x in {((sup the carrier' of J) +^ 1),((sup the carrier' of J) +^ 2),((sup the carrier' of J) +^ 3),((sup the carrier' of J) +^ 4)} & x in {((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:] ) by XBOOLE_0:3;
A3: ( x = (sup the carrier' of J) +^ 1 or x = (sup the carrier' of J) +^ 2 or x = (sup the carrier' of J) +^ 3 or x = (sup the carrier' of J) +^ 4 ) by ;
A4: ( (sup the carrier' of J) +^ 0 <> (sup the carrier' of J) +^ 1 & (sup the carrier' of J) +^ 0 <> (sup the carrier' of J) +^ 2 & (sup the carrier' of J) +^ 0 <> (sup the carrier' of J) +^ 3 & (sup the carrier' of J) +^ 0 <> (sup the carrier' of J) +^ 4 ) by ORDINAL3:21;
( x in {((sup the carrier' of J) +^ 0)} or x in [:{ the carrier' of J},{1,2},X:] ) by ;
then consider j, y, z being object such that
A5: ( j in { the carrier' of J} & y in {1,2} & z in X & x = [j,y,z] ) by ;
thus contradiction by A2, A5, ENUMSET1:def 2; :: thesis: verum
end;
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 ;
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
.= ({((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)}
proof
assume {((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:] meets {((sup the carrier' of J) +^ 5)} ; :: thesis: contradiction
then consider x being object such that
A7: ( x 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)} \/ [:{ the carrier' of J},{1,2},X:] & x in {((sup the carrier' of J) +^ 5)} ) by XBOOLE_0:3;
A8: ( (sup the carrier' of J) +^ 5 <> (sup the carrier' of J) +^ 0 & (sup the carrier' of J) +^ 5 <> (sup the carrier' of J) +^ 1 & (sup the carrier' of J) +^ 5 <> (sup the carrier' of J) +^ 2 & (sup the carrier' of J) +^ 5 <> (sup the carrier' of J) +^ 3 & (sup the carrier' of J) +^ 5 <> (sup the carrier' of J) +^ 4 ) by ORDINAL3:21;
x = (sup the carrier' of J) +^ 5 by ;
then ( (sup the carrier' of J) +^ 5 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)} or (sup the carrier' of J) +^ 5 in [:{ the carrier' of J},{1,2},X:] ) by ;
then ex j, y, z being object st
( j in { the carrier' of J} & y in {1,2} & z in X & (sup the carrier' of J) +^ 5 = [j,y,z] ) by ;
hence contradiction ; :: thesis: verum
end;
then reconsider ab = aa \/ ({((sup the carrier' of J) +^ 5)} --> {}) as Function by ;
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
.= ({((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)}
proof
assume {((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:] meets {((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} ; :: thesis: contradiction
then consider x being object such that
A10: ( x 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)} \/ [:{ the carrier' of J},{1,2},X:] & x in {((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} ) by XBOOLE_0:3;
A11: ( (sup the carrier' of J) +^ 6 <> (sup the carrier' of J) +^ 0 & (sup the carrier' of J) +^ 6 <> (sup the carrier' of J) +^ 1 & (sup the carrier' of J) +^ 6 <> (sup the carrier' of J) +^ 2 & (sup the carrier' of J) +^ 6 <> (sup the carrier' of J) +^ 3 & (sup the carrier' of J) +^ 6 <> (sup the carrier' of J) +^ 4 & (sup the carrier' of J) +^ 6 <> (sup the carrier' of J) +^ 5 ) by ORDINAL3:21;
A12: ( (sup the carrier' of J) +^ 7 <> (sup the carrier' of J) +^ 0 & (sup the carrier' of J) +^ 7 <> (sup the carrier' of J) +^ 1 & (sup the carrier' of J) +^ 7 <> (sup the carrier' of J) +^ 2 & (sup the carrier' of J) +^ 7 <> (sup the carrier' of J) +^ 3 & (sup the carrier' of J) +^ 7 <> (sup the carrier' of J) +^ 4 & (sup the carrier' of J) +^ 7 <> (sup the carrier' of J) +^ 5 ) by ORDINAL3:21;
A13: ( (sup the carrier' of J) +^ 8 <> (sup the carrier' of J) +^ 0 & (sup the carrier' of J) +^ 8 <> (sup the carrier' of J) +^ 1 & (sup the carrier' of J) +^ 8 <> (sup the carrier' of J) +^ 2 & (sup the carrier' of J) +^ 8 <> (sup the carrier' of J) +^ 3 & (sup the carrier' of J) +^ 8 <> (sup the carrier' of J) +^ 4 & (sup the carrier' of J) +^ 8 <> (sup the carrier' of J) +^ 5 ) by ORDINAL3:21;
( x = (sup the carrier' of J) +^ 6 or x = (sup the carrier' of J) +^ 7 or x = (sup the carrier' of J) +^ 8 ) by ;
then ( (sup the carrier' of J) +^ 6 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)} or (sup the carrier' of J) +^ 6 in [:{ the carrier' of J},{1,2},X:] or (sup the carrier' of J) +^ 7 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)} or (sup the carrier' of J) +^ 7 in [:{ the carrier' of J},{1,2},X:] or (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)} or (sup the carrier' of J) +^ 8 in [:{ the carrier' of J},{1,2},X:] ) by ;
then ( (sup the carrier' of J) +^ 6 in [:{ the carrier' of J},{1,2},X:] or (sup the carrier' of J) +^ 7 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)} or (sup the carrier' of J) +^ 7 in [:{ the carrier' of J},{1,2},X:] or (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)} or (sup the carrier' of J) +^ 8 in [:{ the carrier' of J},{1,2},X:] ) by ;
then ( (sup the carrier' of J) +^ 6 in [:{ the carrier' of J},{1,2},X:] or (sup the carrier' of J) +^ 7 in [:{ the carrier' of J},{1,2},X:] or (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)} or (sup the carrier' of J) +^ 8 in [:{ the carrier' of J},{1,2},X:] ) by ;
then ( ex j, y, z being object st
( j in { the carrier' of J} & y in {1,2} & z in X & (sup the carrier' of J) +^ 6 = [j,y,z] ) or ex j, y, z being object st
( j in { the carrier' of J} & y in {1,2} & z in X & (sup the carrier' of J) +^ 7 = [j,y,z] ) or ex j, y, z being object st
( j in { the carrier' of J} & y in {1,2} & z in X & (sup the carrier' of J) +^ 8 = [j,y,z] ) ) by ;
hence contradiction ; :: thesis: verum
end;
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 ;
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
.= ({((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 ;
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
proof
assume {((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:] meets the carrier' of J ; :: thesis: contradiction
then consider x being object such that
A18: ( x 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:] & x in the carrier' of J ) by XBOOLE_0:3;
( x 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)} or x in [:{ the carrier' of J},{1,2},X:] ) by ;
then ( not not x = (sup the carrier' of J) +^ 0 & ... & not x = (sup the carrier' of J) +^ 8 or x in [:{ the carrier' of J},{1,2},X:] ) by ENUMSET1:def 7;
then ( ( not not (sup the carrier' of J) +^ 0 in sup the carrier' of J & ... & not (sup the carrier' of J) +^ 8 in sup the carrier' of J & sup the carrier' of J = (sup the carrier' of J) +^ 0 ) or x in [:{ the carrier' of J},{1,2},X:] ) by ;
then consider j, i, y being object such that
A19: ( j in { the carrier' of J} & i in {1,2} & y in X & x = [j,i,y] ) by ;
reconsider jiy = [j,i,y] as set ;
( the carrier' of J = j & j in {j} & {j} in {{j,i},{j}} & {{j,i},{j}} in {[j,i]} & {[j,i]} in jiy ) by ;
hence contradiction by A18, A19, XREGULAR:9; :: thesis: verum
end;
then reconsider ay = the Arity of J \/ a as Function by ;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
( 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 ;
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 ;
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 ;
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 ;
A23: for i being natural number st not not i = 0 & ... & not i = 8 holds
c . (n + i) = (sup the carrier' of J) +^ i
proof
let i be natural number ; :: thesis: ( not not i = 0 & ... & not i = 8 implies c . (n + i) = (sup the carrier' of J) +^ i )
assume not not i = 0 & ... & not i = 8 ; :: thesis: c . (n + i) = (sup the carrier' of J) +^ i
then A24: not ( not i = 0 or not c . (n + 0) = (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>) . (0 + 1) ) & ... & ( not i = 8 or not c . (n + 8) = (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>) . (8 + 1) ) ;
thus c . (n + i) = (sup the carrier' of J) +^ i by ; :: thesis: verum
end;
deffunc H1( 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 = H1(x) ) ) from 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:])
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in 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:]) )
assume x in rng q ; :: thesis: x in 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 consider y being object such that
A26: ( y in dom q & x = q . y ) by FUNCT_1:def 3;
consider i, z being object such that
A27: ( i in {1,2} & z in X & y = [i,z] ) by ;
( x = [ the carrier' of J,(y `1),(y `2)] & y `1 = i & y `2 = z & the carrier' of J in { the carrier' of J} ) by ;
then x in [:{ the carrier' of J},{1,2},X:] by ;
then x 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;
hence x in 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; :: thesis: verum
end;
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 ;
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 ;
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:] ) )
proof
let x be object ; :: according to FUNCT_1:def 4 :: thesis: for b1 being object holds
( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not b1 in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . b1 or x = b1 )

let y be object ; :: thesis: ( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not y in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . y or x = y )
assume A29: ( x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) & y in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) & ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . y ) ; :: thesis: x = y
then A30: ( x in {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} & y in {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} ) by RELAT_1:57;
then A31: ( c . x = (c | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x & (c | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = c . y ) by ;
A32: ( not not x = n + 0 & ... & not x = n + 5 & not not y = n + 0 & ... & not y = n + 5 ) by ;
then consider i being Nat such that
A33: ( 0 <= i & i <= 5 & x = n + i ) ;
consider j being Nat such that
A34: ( 0 <= j & j <= 5 & y = n + j ) by A32;
( i <= 8 & j <= 8 ) by ;
then ( not not i = 0 & ... & not i = 8 & not not j = 0 & ... & not j = 8 ) ;
then ( c . x = (sup the carrier' of J) +^ i & c . y = (sup the carrier' of J) +^ j ) by ;
hence x = y by ; :: thesis: verum
end;
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:] ) )
proof
not not 0 = 0 & ... & not 0 = 8 ;
then A35: c . (n + 0) = (sup the carrier' of J) +^ 0 by A23;
A36: ( (sup the carrier' of J) +^ 0 in {((sup the carrier' of J) +^ 0)} & 00 in {00} ) by TARSKI:def 1;
then ( (sup the carrier' of J) +^ 0 in {((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:] & <*00*> in {<*00*>} ) by ;
then [((sup the carrier' of J) +^ 0),<*00*>] in ({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*00*> by ZFMISC_1:106;
then [((sup the carrier' of J) +^ 0),<*00*>] in aa by XBOOLE_0:def 3;
then [((sup the carrier' of J) +^ 0),<*00*>] in ab by XBOOLE_0:def 3;
then [((sup the carrier' of J) +^ 0),<*00*>] in a by XBOOLE_0:def 3;
then [((sup the carrier' of J) +^ 0),<*00*>] in ay by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . n) = <* the formula-sort of L*> by ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . n) = the formula-sort of L
(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)} by ENUMSET1:def 7;
then A37: (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:] by XBOOLE_0:def 3;
then [((sup the carrier' of J) +^ 0),00] 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) +^ 0) by ;
then (({((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 . n) = 00 by ;
hence the ResultSort of L . ( the connectives of L . n) = the formula-sort of L by ; :: thesis: verum
end;
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:] ) )
proof
not not 5 = 0 & ... & not 5 = 8 ;
then A38: c . (n + 5) = (sup the carrier' of J) +^ 5 by A23;
( (sup the carrier' of J) +^ 5 in {((sup the carrier' of J) +^ 5)} & {} in ) by TARSKI:def 1;
then [((sup the carrier' of J) +^ 5),{}] in {((sup the carrier' of J) +^ 5)} --> {} by ZFMISC_1:106;
then [((sup the carrier' of J) +^ 5),{}] in ab by XBOOLE_0:def 3;
then [((sup the carrier' of J) +^ 5),{}] in a by XBOOLE_0:def 3;
then [((sup the carrier' of J) +^ 5),{}] in ay by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . (n + 5)) = {} by ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . (n + 5)) = the formula-sort of L
(sup the carrier' of J) +^ 5 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 A39: ( (sup the carrier' of J) +^ 5 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:] & 00 in {00} ) by ;
then [((sup the carrier' of J) +^ 5),00] 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) +^ 0) by ZFMISC_1:87;
then (({((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) +^ 5) = 00 by FUNCT_1:1;
hence the ResultSort of L . ( the connectives of L . (n + 5)) = the formula-sort of L by ; :: thesis: verum
end;
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:] ) )
proof
let i be natural number ; :: thesis: ( not 1 <= i or not i <= 4 or the connectives of L . (n + i) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L )
assume A40: ( 1 <= i & i <= 4 ) ; :: thesis: the connectives of L . (n + i) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L
then ( 0 <= i & i <= 8 ) by XXREAL_0:2;
then A41: not not i = 0 & ... & not i = 8 ;
then A42: c . (n + i) = (sup the carrier' of J) +^ i by A23;
not not i = 1 & ... & not i = 4 by A40;
then ( c . (n + i) in {((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*> in {<*00,00*>} ) by ;
then [(c . (n + i)),<*00,00*>] in {((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*> by ZFMISC_1:106;
then [(c . (n + i)),<*00,00*>] in aa by XBOOLE_0:def 3;
then [(c . (n + i)),<*00,00*>] in ab by XBOOLE_0:def 3;
then [(c . (n + i)),<*00,00*>] in a by XBOOLE_0:def 3;
then [(c . (n + i)),<*00,00*>] in ay by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . (n + i)) = <* the formula-sort of L, the formula-sort of L*> by FUNCT_1:1; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . (n + i)) = the formula-sort of L
c . (n + i) 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 ;
then A43: ( c . (n + i) 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:] & 00 in {00} ) by ;
then [(c . (n + i)),00] 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) +^ 0) by ZFMISC_1:106;
then (({((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 . (n + i)) = 00 by FUNCT_1:1;
hence the ResultSort of L . ( the connectives of L . (n + i)) = the formula-sort of L by ; :: thesis: verum
end;
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:] ) )
proof
let x be object ; :: according to FUNCT_1:def 4 :: thesis: for b1 being object holds
( not x in dom the quantifiers of L or not b1 in dom the quantifiers of L or not the quantifiers of L . x = the quantifiers of L . b1 or x = b1 )

let y be object ; :: thesis: ( not x in dom the quantifiers of L or not y in dom the quantifiers of L or not the quantifiers of L . x = the quantifiers of L . y or x = y )
assume A44: ( x in dom the quantifiers of L & y in dom the quantifiers of L ) ; :: thesis: ( not the quantifiers of L . x = the quantifiers of L . y or x = y )
then reconsider a = x, b = y as Element of [:{1,2},X:] ;
assume the quantifiers of L . x = the quantifiers of L . y ; :: thesis: x = y
then [ the carrier' of J,(x `1),(x `2)] = the quantifiers of L . y by
.= [ the carrier' of J,(y `1),(y `2)] by ;
then ( x `1 = y `1 & x `2 = y `2 ) by XTUPLE_0:3;
then ( x = [(a `1),(a `2)] & [(a `1),(a `2)] = [(b `1),(b `2)] & [(b `1),(b `2)] = y ) ;
hence x = y ; :: thesis: verum
end;
rng the quantifiers of L c= [:{ the carrier' of J},{1,2},X:]
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng the quantifiers of L or a in [:{ the carrier' of J},{1,2},X:] )
assume a in rng the quantifiers of L ; :: thesis: a in [:{ the carrier' of J},{1,2},X:]
then consider b being object such that
C1: ( b in dom the quantifiers of L & a = the quantifiers of L . b ) by FUNCT_1:def 3;
reconsider b = b as Element of [:{1,2},X:] by C1;
( a = [ the carrier' of J,(b `1),(b `2)] & b `1 in {1,2} & b `2 in X & the carrier' of J in { the carrier' of J} ) by ;
hence a in [:{ the carrier' of J},{1,2},X:] by MCART_1:69; :: thesis: verum
end;
hence rng the quantifiers of L misses rng the connectives of L by ; :: 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:] ) )

hereby :: thesis: ( 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:] ) )
let q, x be object ; :: thesis: ( q in the quant-sort of L & x in X implies the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L )
assume A45: ( q in the quant-sort of L & x in X ) ; :: thesis: the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L
A46: ( the quantifiers of L . (q,x) = [ the carrier' of J,([q,x] `1),([q,x] `2)] & <*00*> in {<*00*>} & [q,x] `1 = q & [q,x] `2 = x & the carrier' of J in { the carrier' of J} ) by ;
then the quantifiers of L . (q,x) in [:{ the carrier' of J}, the quant-sort of L,X:] by ;
then ( the quantifiers of L . (q,x) in {((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:] & <*00*> in {<*00*>} ) by ;
then [( the quantifiers of L . (q,x)),<*00*>] in ({((sup the carrier' of J) +^ 0)} \/ [:{ the carrier' of J},{1,2},X:]) --> <*00*> by ZFMISC_1:106;
then [( the quantifiers of L . (q,x)),<*00*>] in aa by XBOOLE_0:def 3;
then [( the quantifiers of L . (q,x)),<*00*>] in ab by XBOOLE_0:def 3;
then [( the quantifiers of L . (q,x)),<*00*>] in a by XBOOLE_0:def 3;
then A47: [( the quantifiers of L . (q,x)),<*00*>] in ay by XBOOLE_0:def 3;
thus the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L :: thesis: verum
proof
thus the Arity of L . ( the quantifiers of L . (q,x)) = <* the formula-sort of L*> by ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the quantifiers of L . (q,x)) = the formula-sort of L
[ the carrier' of J,q,x] in [:{ the carrier' of J},{1,2},X:] by ;
then A48: [ the carrier' of J,q,x] 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 ( (({((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,q,x] = 00 & [ the carrier' of J,q,x] in 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 ;
hence the ResultSort of L . ( the quantifiers of L . (q,x)) = the formula-sort of L by ; :: thesis: verum
end;
end;
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 ; :: 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:] ) )
proof
let i be natural number ; :: thesis: ( not 6 <= i or not i <= 8 or the connectives of L . (n + i) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L )
assume A49: ( 6 <= i & i <= 8 ) ; :: thesis: the connectives of L . (n + i) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L
A50: not not i = 0 & ... & not i = 8 by A49;
then A51: c . (n + i) = (sup the carrier' of J) +^ i by A23;
not not i = 6 & ... & not i = 8 by A49;
then ( (sup the carrier' of J) +^ i in {((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} & <*01,00*> in {<*01,00*>} ) by ;
then [((sup the carrier' of J) +^ i),<*01,00*>] in {((sup the carrier' of J) +^ 6),((sup the carrier' of J) +^ 7),((sup the carrier' of J) +^ 8)} --> <*01,00*> by ZFMISC_1:106;
then [((sup the carrier' of J) +^ i),<*01,00*>] in a by XBOOLE_0:def 3;
then [((sup the carrier' of J) +^ i),<*01,00*>] in ay by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . (n + i)) = <* the program-sort of L, the formula-sort of L*> by ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . (n + i)) = the formula-sort of L
(sup the carrier' of J) +^ i 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 ;
then A52: (sup the carrier' of J) +^ i 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 [((sup the carrier' of J) +^ i),00] 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) +^ 0) by ZFMISC_1:106;
then (({((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) +^ i) = 00 by FUNCT_1:1;
hence the ResultSort of L . ( the connectives of L . (n + i)) = the formula-sort of L by ; :: thesis: verum
end;
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:] ) )
proof
set f1 = id the carrier of J;
set g1 = id the carrier' of J;
thus ( dom (id the carrier of J) = the carrier of J & dom (id the carrier' of J) = the carrier' of J ) ; :: according to PUA2MSS1:def 12,INSTALG1:def 2,AOFA_L00:def 2 :: thesis: ( rng (id the carrier of J) c= the carrier of L & rng (id the carrier' of J) c= the carrier' of L & the ResultSort of J * (id the carrier of J) = (id the carrier' of J) * the ResultSort of L & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of J or not b2 = the Arity of J . b1 or b2 * (id the carrier of J) = the Arity of L . ((id the carrier' of J) . b1) ) ) )

thus ( rng (id the carrier of J) c= the carrier of L & rng (id the carrier' of J) c= the carrier' of L ) by XBOOLE_1:7; :: thesis: ( the ResultSort of J * (id the carrier of J) = (id the carrier' of J) * the ResultSort of L & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of J or not b2 = the Arity of J . b1 or b2 * (id the carrier of J) = the Arity of L . ((id the carrier' of J) . b1) ) ) )

( the carrier' of J <> {} implies the carrier of J <> {} ) by INSTALG1:def 1;
then A53: ( dom the ResultSort of J = the carrier' of J & dom the Arity of J = the carrier' of J ) by FUNCT_2:def 1;
rng the ResultSort of J c= the carrier of J ;
hence (id the carrier of J) * the ResultSort of J = the ResultSort of J by RELAT_1:53
.= the ResultSort of L | the carrier' of J by
.= the ResultSort of L * (id the carrier' of J) by RELAT_1:65 ;
:: thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of J or not b2 = the Arity of J . b1 or b2 * (id the carrier of J) = the Arity of L . ((id the carrier' of J) . b1) )

let o be set ; :: thesis: for b1 being set holds
( not o in the carrier' of J or not b1 = the Arity of J . o or b1 * (id the carrier of J) = the Arity of L . ((id the carrier' of J) . o) )

let p be Function; :: thesis: ( not o in the carrier' of J or not p = the Arity of J . o or p * (id the carrier of J) = the Arity of L . ((id the carrier' of J) . o) )
assume A54: o in the carrier' of J ; :: thesis: ( not p = the Arity of J . o or p * (id the carrier of J) = the Arity of L . ((id the carrier' of J) . o) )
then reconsider x = o as Element of the carrier' of J ;
assume A55: p = the Arity of J . o ; :: thesis: p * (id the carrier of J) = the Arity of L . ((id the carrier' of J) . o)
dom the Arity of J = the carrier' of J by FUNCT_2:def 1;
then reconsider q = p as Element of the carrier of J * by ;
rng q c= the carrier of J ;
then ( (id the carrier of J) * p = p & (id the carrier' of J) . x = x ) by RELAT_1:53;
hence (id the carrier of J) * p = the Arity of L . ((id the carrier' of J) . o) by ; :: thesis: verum
end;
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:] ) )

hereby :: thesis: ( 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:] ) )
let x be Element of X; :: thesis: ( the quantifiers of L . (1,x) = [ the carrier' of J,1,x] & the quantifiers of L . (2,x) = [ the carrier' of J,2,x] )
1 in {1,2} by TARSKI:def 2;
then [1,x] in [:{1,2},X:] by ZFMISC_1:def 2;
hence the quantifiers of L . (1,x) = [ the carrier' of J,([1,x] `1),([1,x] `2)] by A25
.= [ the carrier' of J,1,x] ;
:: thesis: the quantifiers of L . (2,x) = [ the carrier' of J,2,x]
2 in {1,2} by TARSKI:def 2;
then [2,x] in [:{1,2},X:] by ZFMISC_1:def 2;
hence the quantifiers of L . (2,x) = [ the carrier' of J,([2,x] `1),([2,x] `2)] by A25
.= [ the carrier' of J,2,x] ;
:: thesis: verum
end;
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