let n be natural non empty number ; 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 ; 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; 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:]
;
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 A2, ENUMSET1:def 7;
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 A2, MCART_1:68;
thus
contradiction
by A3, A5;
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:]
;
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 A2, ENUMSET1:def 2;
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 A2, XBOOLE_0:def 3;
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 A3, A4, MCART_1:68, TARSKI:def 1;
thus
contradiction
by A2, A5, ENUMSET1:def 2;
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 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)}
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)}
;
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 A7, TARSKI:def 1;
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 A7, XBOOLE_0:def 3;
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 A8, ENUMSET1:def 3, MCART_1:68;
hence
contradiction
;
verum
end;
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)}
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)}
;
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 A10, ENUMSET1:def 1;
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 A10, XBOOLE_0:def 3;
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 A11, ENUMSET1:def 4;
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 A12, ENUMSET1:def 4;
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 A13, ENUMSET1:def 4, MCART_1:68;
hence
contradiction
;
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 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
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
;
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 A18, XBOOLE_0:def 3;
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 A18, ORDINAL2:19, ORDINAL2:27;
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 MCART_1:68, ORDINAL3:22;
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 A19, TARSKI:def 1, TARSKI:def 2;
hence
contradiction
by A18, A19, XREGULAR:9;
verum
end;
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 m = n -' 1;
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;
then
n - 1 >= 1 - 1
by XREAL_1:9;
then bb:
n -' 1 = n - 1
by XREAL_0:def 2;
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
proof
let i be
natural number ;
( not not i = 0 & ... & not i = 8 implies c . (n + i) = (sup the carrier' of J) +^ i )
aaa:
c . ((n -' 1) + 1) = (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>) . 1 & ... &
c . ((n -' 1) + 9) = (<*o0,o1,o2,o3,o4,o5,o6,o7*> ^ <*o8*>) . 9
by FINSEQ_3:155;
assume
not not
i = 0 & ... & not
i = 8
;
c . (n + i) = (sup the carrier' of J) +^ i
then
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) )
by aaa, bb;
hence
c . (n + i) = (sup the carrier' of J) +^ i
by AOFA_A00:29;
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 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:])
proof
let x be
object ;
TARSKI:def 3 ( 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
;
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 A25, A26, ZFMISC_1:def 2;
(
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 A25, A26, A27, TARSKI:def 1;
then
x in [:{ the carrier' of J},{1,2},X:]
by A27, MCART_1:69;
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;
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 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
; ( 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; AOFA_L00:def 4 ( 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
( 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 ;
FUNCT_1:def 4 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 ;
( 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 )
;
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 A29, FUNCT_1:49;
A32:
( not not
x = n + 0 & ... & not
x = n + 5 & not not
y = n + 0 & ... & not
y = n + 5 )
by A30, ENUMSET1:def 4;
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 A33, A34, XXREAL_0:2;
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 A23, A33, A34;
hence
x = y
by A31, A33, A34, ORDINAL3:21;
verum
end;
thus
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
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 XBOOLE_0:def 3, TARSKI:def 1;
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 A35, FUNCT_1:1;
AOFA_A00:def 8 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 A36, 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)) . (c . n) = 00
by A35, FUNCT_1:1;
hence
the
ResultSort of
L . ( the connectives of L . n) = the
formula-sort of
L
by A35, A37, A21, FUNCT_4:13;
verum
end;
thus
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 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 A38, FUNCT_1:1;
AOFA_A00:def 8 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 TARSKI:def 1, XBOOLE_0:def 3;
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 A39, A38, A21, FUNCT_4:13;
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
( 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 ;
( 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 )
;
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 A42, TARSKI:def 1, ENUMSET1:def 2;
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;
AOFA_A00:def 8 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 A42, A41, ENUMSET1:def 7;
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 TARSKI:def 1, XBOOLE_0:def 3;
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 A43, A21, FUNCT_4:13;
verum
end;
thus
the quant-sort of L = {1,2}
; AOFA_L00:def 5 ( 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
( 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 ;
FUNCT_1:def 4 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 ;
( 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 )
;
( 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
;
x = y
then [ the carrier' of J,(x `1),(x `2)] =
the
quantifiers of
L . y
by A44, A25
.=
[ the carrier' of J,(y `1),(y `2)]
by A44, A25
;
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
;
verum
end;
rng the quantifiers of L c= [:{ the carrier' of J},{1,2},X:]
proof
let a be
object ;
TARSKI:def 3 ( 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
;
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 C1, A25, TARSKI:def 1, MCART_1:10;
hence
a in [:{ the carrier' of J},{1,2},X:]
by MCART_1:69;
verum
end;
hence
rng the quantifiers of L misses rng the connectives of L
by B1, B3, XBOOLE_1:64; ( ( 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 ( 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 ;
( 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 )
;
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of LA46:
( 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 A25, A45, TARSKI:def 1, ZFMISC_1:87;
then
the
quantifiers of
L . (
q,
x)
in [:{ the carrier' of J}, the quant-sort of L,X:]
by A45, MCART_1:69;
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 XBOOLE_0:def 3, TARSKI:def 1;
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
verumproof
thus
the
Arity of
L . ( the quantifiers of L . (q,x)) = <* the formula-sort of L*>
by A47, FUNCT_1:1;
AOFA_A00:def 8 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 A46, A45, MCART_1:69;
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 XBOOLE_0:def 3, FUNCOP_1:7;
hence
the
ResultSort of
L . ( the quantifiers of L . (q,x)) = the
formula-sort of
L
by A21, A46, A48, FUNCT_4:13;
verum
end;
end;
thus
the program-sort of L <> the formula-sort of L
by ORDINAL3:21; AOFA_L00:def 6 ( 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; ( 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
( 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 ;
( 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 )
;
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 TARSKI:def 1, ENUMSET1:def 1;
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 A51, FUNCT_1:1;
AOFA_A00:def 8 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 A50, ENUMSET1:def 7;
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 A21, A52, A51, FUNCT_4:13;
verum
end;
thus
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
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; ( ( 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 ( 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;
( 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]
;
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]
;
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; ( 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}
; 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; ( 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
; 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; verum