:: Recursive Definitions. {P}art {II}
:: by Artur Korni{\l}owicz
::
:: Received February 10, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users

begin

definition

let x be set ;
given x1, x2, x3 being set such that A1: x = [x1,x2,x3] ;
func x `1_3 -> set means :Def1: :: RECDEF_2:def 1
for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y1;
existence
ex b₁ being set st
for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₁ = y1

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₁ = y1 ) & ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₂ = y1 ) holds
b₁ = b₂

proof end;

func x `2_3 -> set means :Def2: :: RECDEF_2:def 2
for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y2;
existence
ex b₁ being set st
for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₁ = y2

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₁ = y2 ) & ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₂ = y2 ) holds
b₁ = b₂

proof end;

func x `3_3 -> set means :Def3: :: RECDEF_2:def 3
for y1, y2, y3 being set st x = [y1,y2,y3] holds
it = y3;
existence
ex b₁ being set st
for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₁ = y3

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₁ = y3 ) & ( for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₂ = y3 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines `1_3 RECDEF_2:def 1 :
for x being set st ex x1, x2, x3 being set st x = [x1,x2,x3] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `1_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₂ = y1 );

:: deftheorem Def2 defines `2_3 RECDEF_2:def 2 :
for x being set st ex x1, x2, x3 being set st x = [x1,x2,x3] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `2_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₂ = y2 );

:: deftheorem Def3 defines `3_3 RECDEF_2:def 3 :
for x being set st ex x1, x2, x3 being set st x = [x1,x2,x3] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `3_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b₂ = y3 );

theorem Th1: :: RECDEF_2:1

for z being set st ex a, b, c being set st z = [a,b,c] holds
z = [(z `1_3),(z `2_3),(z `3_3)]

proof end;

theorem :: RECDEF_2:2

for z, A, B, C being set st z in [:A,B,C:] holds
( z `1_3 in A & z `2_3 in B & z `3_3 in C )

proof end;

theorem Th3: :: RECDEF_2:3

for z, A, B, C being set st z in [:A,B,C:] holds
z = [(z `1_3),(z `2_3),(z `3_3)]

proof end;

definition

let x be set ;
given x1, x2, x3, x4 being set such that A1: x = [x1,x2,x3,x4] ;
func x `1_4 -> set means :Def4: :: RECDEF_2:def 4
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y1;
existence
ex b₁ being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y1

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y1 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y1 ) holds
b₁ = b₂

proof end;

func x `2_4 -> set means :Def5: :: RECDEF_2:def 5
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y2;
existence
ex b₁ being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y2

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y2 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y2 ) holds
b₁ = b₂

proof end;

func x `3_4 -> set means :Def6: :: RECDEF_2:def 6
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y3;
existence
ex b₁ being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y3

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y3 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y3 ) holds
b₁ = b₂

proof end;

func x `4_4 -> set means :Def7: :: RECDEF_2:def 7
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
it = y4;
existence
ex b₁ being set st
for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y4

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₁ = y4 ) & ( for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y4 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines `1_4 RECDEF_2:def 4 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `1_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y1 );

:: deftheorem Def5 defines `2_4 RECDEF_2:def 5 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `2_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y2 );

:: deftheorem Def6 defines `3_4 RECDEF_2:def 6 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `3_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y3 );

:: deftheorem Def7 defines `4_4 RECDEF_2:def 7 :
for x being set st ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `4_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b₂ = y4 );

theorem Th4: :: RECDEF_2:4

for z being set st ex a, b, c, d being set st z = [a,b,c,d] holds
z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]

proof end;

theorem :: RECDEF_2:5

for z, A, B, C, D being set st z in [:A,B,C,D:] holds
( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D )

proof end;

theorem :: RECDEF_2:6

for z, A, B, C, D being set st z in [:A,B,C,D:] holds
z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]

proof end;

definition

let x be set ;
given x1, x2, x3, x4, x5 being set such that A1: x = [x1,x2,x3,x4,x5] ;
func x `1_5 -> set means :Def8: :: RECDEF_2:def 8
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y1;
existence
ex b₁ being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y1

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y1 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y1 ) holds
b₁ = b₂

proof end;

func x `2_5 -> set means :Def9: :: RECDEF_2:def 9
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y2;
existence
ex b₁ being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y2

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y2 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y2 ) holds
b₁ = b₂

proof end;

func x `3_5 -> set means :Def10: :: RECDEF_2:def 10
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y3;
existence
ex b₁ being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y3

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y3 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y3 ) holds
b₁ = b₂

proof end;

func x `4_5 -> set means :Def11: :: RECDEF_2:def 11
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y4;
existence
ex b₁ being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y4

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y4 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y4 ) holds
b₁ = b₂

proof end;

func x `5_5 -> set means :Def12: :: RECDEF_2:def 12
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
it = y5;
existence
ex b₁ being set st
for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y5

proof end;

uniqueness
for b₁, b₂ being set st ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₁ = y5 ) & ( for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y5 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines `1_5 RECDEF_2:def 8 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `1_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y1 );

:: deftheorem Def9 defines `2_5 RECDEF_2:def 9 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `2_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y2 );

:: deftheorem Def10 defines `3_5 RECDEF_2:def 10 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `3_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y3 );

:: deftheorem Def11 defines `4_5 RECDEF_2:def 11 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `4_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y4 );

:: deftheorem Def12 defines `5_5 RECDEF_2:def 12 :
for x being set st ex x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
for b<sub>2</sub> being set holds
( b<sub>2</sub> = x `5_5 iff for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
b₂ = y5 );

theorem Th7: :: RECDEF_2:7

for z being set st ex a, b, c, d, e being set st z = [a,b,c,d,e] holds
z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)]

proof end;

theorem :: RECDEF_2:8

for z, A, B, C, D, E being set st z in [:A,B,C,D,E:] holds
( z `1_5 in A & z `2_5 in B & z `3_5 in C & z `4_5 in D & z `5_5 in E )

proof end;

theorem :: RECDEF_2:9

for z, A, B, C, D, E being set st z in [:A,B,C,D,E:] holds
z = [(z `1_5),(z `2_5),(z `3_5),(z `4_5),(z `5_5)]

proof end;

scheme :: RECDEF_2:sch 1
ExFunc3Cond{ F₁() -> set , P₁[ set ], P₂[ set ], P₃[ set ], F₂( set ) -> set , F₃( set ) -> set , F₄( set ) -> set } :

ex f being Function st
( dom f = F₁() & ( for c being set st c in F₁() holds
( ( P₁[c] implies f . c = F₂(c) ) & ( P₂[c] implies f . c = F₃(c) ) & ( P₃[c] implies f . c = F₄(c) ) ) ) )

provided

A1: for c being set st c in F₁() holds
( ( P₁[c] implies not P₂[c] ) & ( P₁[c] implies not P₃[c] ) & ( P₂[c] implies not P₃[c] ) ) and
A2: for c being set holds
( not c in F₁() or P₁[c] or P₂[c] or P₃[c] )

proof end;

scheme :: RECDEF_2:sch 2
ExFunc4Cond{ F₁() -> set , P₁[ set ], P₂[ set ], P₃[ set ], P₄[ set ], F₂( set ) -> set , F₃( set ) -> set , F₄( set ) -> set , F₅( set ) -> set } :

ex f being Function st
( dom f = F₁() & ( for c being set st c in F₁() holds
( ( P₁[c] implies f . c = F₂(c) ) & ( P₂[c] implies f . c = F₃(c) ) & ( P₃[c] implies f . c = F₄(c) ) & ( P₄[c] implies f . c = F₅(c) ) ) ) )

provided

A1: for c being set st c in F₁() holds
( ( P₁[c] implies not P₂[c] ) & ( P₁[c] implies not P₃[c] ) & ( P₁[c] implies not P₄[c] ) & ( P₂[c] implies not P₃[c] ) & ( P₂[c] implies not P₄[c] ) & ( P₃[c] implies not P₄[c] ) ) and
A2: for c being set holds
( not c in F₁() or P₁[c] or P₂[c] or P₃[c] or P₄[c] )

proof end;

scheme :: RECDEF_2:sch 3
DoubleChoiceRec{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₂(), P₁[ set , set , set , set , set ] } :

ex f being Function of NAT,F₁() ex g being Function of NAT,F₂() st
( f . 0 = F₃() & g . 0 = F₄() & ( for n being Element of NAT holds P₁[n,f . n,g . n,f . (n + 1),g . (n + 1)] ) )

provided

A1: for n being Element of NAT
for x being Element of F₁()
for y being Element of F₂() ex x1 being Element of F₁() ex y1 being Element of F₂() st P₁[n,x,y,x1,y1]

proof end;

scheme :: RECDEF_2:sch 4
LambdaRec2Ex{ F₁() -> set , F₂() -> set , F₃( set , set , set ) -> set } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & f . 1 = F₂() & ( for n being Element of NAT holds f . (n + 2) = F₃(n,(f . n),(f . (n + 1))) ) )

proof end;

scheme :: RECDEF_2:sch 5
LambdaRec2ExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄( set , set , set ) -> Element of F₁() } :

ex f being Function of NAT,F₁() st
( f . 0 = F₂() & f . 1 = F₃() & ( for n being Element of NAT holds f . (n + 2) = F₄(n,(f . n),(f . (n + 1))) ) )

proof end;

scheme :: RECDEF_2:sch 6
LambdaRec2Un{ F₁() -> set , F₂() -> set , F₃() -> Function, F₄() -> Function, F₅( set , set , set ) -> set } :

F₃() = F₄()

provided

A1: dom F₃() = NAT and
A2: ( F₃() . 0 = F₁() & F₃() . 1 = F₂() ) and
A3: for n being Element of NAT holds F₃() . (n + 2) = F₅(n,(F₃() . n),(F₃() . (n + 1))) and
A4: dom F₄() = NAT and
A5: ( F₄() . 0 = F₁() & F₄() . 1 = F₂() ) and
A6: for n being Element of NAT holds F₄() . (n + 2) = F₅(n,(F₄() . n),(F₄() . (n + 1)))

proof end;

scheme :: RECDEF_2:sch 7
LambdaRec2UnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Function of NAT,F₁(), F₅() -> Function of NAT,F₁(), F₆( set , set , set ) -> Element of F₁() } :

F₄() = F₅()

provided

A1: ( F₄() . 0 = F₂() & F₄() . 1 = F₃() ) and
A2: for n being Element of NAT holds F₄() . (n + 2) = F₆(n,(F₄() . n),(F₄() . (n + 1))) and
A3: ( F₅() . 0 = F₂() & F₅() . 1 = F₃() ) and
A4: for n being Element of NAT holds F₅() . (n + 2) = F₆(n,(F₅() . n),(F₅() . (n + 1)))

proof end;

scheme :: RECDEF_2:sch 8
LambdaRec3Ex{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set , set , set ) -> set } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & f . 1 = F₂() & f . 2 = F₃() & ( for n being Element of NAT holds f . (n + 3) = F₄(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )

proof end;

scheme :: RECDEF_2:sch 9
LambdaRec3ExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅( set , set , set , set ) -> Element of F₁() } :

ex f being Function of NAT,F₁() st
( f . 0 = F₂() & f . 1 = F₃() & f . 2 = F₄() & ( for n being Element of NAT holds f . (n + 3) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )

proof end;

scheme :: RECDEF_2:sch 10
LambdaRec3Un{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> Function, F₅() -> Function, F₆( set , set , set , set ) -> set } :

F₄() = F₅()

provided

A1: dom F₄() = NAT and
A2: ( F₄() . 0 = F₁() & F₄() . 1 = F₂() & F₄() . 2 = F₃() ) and
A3: for n being Element of NAT holds F₄() . (n + 3) = F₆(n,(F₄() . n),(F₄() . (n + 1)),(F₄() . (n + 2))) and
A4: dom F₅() = NAT and
A5: ( F₅() . 0 = F₁() & F₅() . 1 = F₂() & F₅() . 2 = F₃() ) and
A6: for n being Element of NAT holds F₅() . (n + 3) = F₆(n,(F₅() . n),(F₅() . (n + 1)),(F₅() . (n + 2)))

proof end;

scheme :: RECDEF_2:sch 11
LambdaRec3UnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Function of NAT,F₁(), F₆() -> Function of NAT,F₁(), F₇( set , set , set , set ) -> Element of F₁() } :

F₅() = F₆()

provided

A1: ( F₅() . 0 = F₂() & F₅() . 1 = F₃() & F₅() . 2 = F₄() ) and
A2: for n being Element of NAT holds F₅() . (n + 3) = F₇(n,(F₅() . n),(F₅() . (n + 1)),(F₅() . (n + 2))) and
A3: ( F₆() . 0 = F₂() & F₆() . 1 = F₃() & F₆() . 2 = F₄() ) and
A4: for n being Element of NAT holds F₆() . (n + 3) = F₇(n,(F₆() . n),(F₆() . (n + 1)),(F₆() . (n + 2)))

proof end;

scheme :: RECDEF_2:sch 12
LambdaRec4Ex{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅( set , set , set , set , set ) -> set } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & f . 1 = F₂() & f . 2 = F₃() & f . 3 = F₄() & ( for n being Element of NAT holds f . (n + 4) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )

proof end;

scheme :: RECDEF_2:sch 13
LambdaRec4ExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₁(), F₆( set , set , set , set , set ) -> Element of F₁() } :

ex f being Function of NAT,F₁() st
( f . 0 = F₂() & f . 1 = F₃() & f . 2 = F₄() & f . 3 = F₅() & ( for n being Element of NAT holds f . (n + 4) = F₆(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )

proof end;

scheme :: RECDEF_2:sch 14
LambdaRec4Un{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> Function, F₆() -> Function, F₇( set , set , set , set , set ) -> set } :

F₅() = F₆()

provided

A1: dom F₅() = NAT and
A2: ( F₅() . 0 = F₁() & F₅() . 1 = F₂() & F₅() . 2 = F₃() & F₅() . 3 = F₄() ) and
A3: for n being Element of NAT holds F₅() . (n + 4) = F₇(n,(F₅() . n),(F₅() . (n + 1)),(F₅() . (n + 2)),(F₅() . (n + 3))) and
A4: dom F₆() = NAT and
A5: ( F₆() . 0 = F₁() & F₆() . 1 = F₂() & F₆() . 2 = F₃() & F₆() . 3 = F₄() ) and
A6: for n being Element of NAT holds F₆() . (n + 4) = F₇(n,(F₆() . n),(F₆() . (n + 1)),(F₆() . (n + 2)),(F₆() . (n + 3)))

proof end;

scheme :: RECDEF_2:sch 15
LambdaRec4UnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₁(), F₆() -> Function of NAT,F₁(), F₇() -> Function of NAT,F₁(), F₈( set , set , set , set , set ) -> Element of F₁() } :

F₆() = F₇()

provided

A1: ( F₆() . 0 = F₂() & F₆() . 1 = F₃() & F₆() . 2 = F₄() & F₆() . 3 = F₅() ) and
A2: for n being Element of NAT holds F₆() . (n + 4) = F₈(n,(F₆() . n),(F₆() . (n + 1)),(F₆() . (n + 2)),(F₆() . (n + 3))) and
A3: ( F₇() . 0 = F₂() & F₇() . 1 = F₃() & F₇() . 2 = F₄() & F₇() . 3 = F₅() ) and
A4: for n being Element of NAT holds F₇() . (n + 4) = F₈(n,(F₇() . n),(F₇() . (n + 1)),(F₇() . (n + 2)),(F₇() . (n + 3)))

proof end;

begin

theorem :: RECDEF_2:10

for x, y, X, Y, Z being set st x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 & y in [:X,Y,Z:] & x in [:X,Y,Z:] holds
x = y

proof end;