:: RECDEF_1 semantic presentation begin Lm1: for n being Element of NAT for D being non empty set for p being FinSequence of D st 1 <= n & n <= len p holds p . n is Element of D proof let n be Element of NAT ; ::_thesis: for D being non empty set for p being FinSequence of D st 1 <= n & n <= len p holds p . n is Element of D let D be non empty set ; ::_thesis: for p being FinSequence of D st 1 <= n & n <= len p holds p . n is Element of D let p be FinSequence of D; ::_thesis: ( 1 <= n & n <= len p implies p . n is Element of D ) assume ( 1 <= n & n <= len p ) ; ::_thesis: p . n is Element of D then n in Seg (len p) by FINSEQ_1:1; then n in dom p by FINSEQ_1:def_3; then A1: p . n in rng p by FUNCT_1:def_3; rng p c= D by FINSEQ_1:def_4; hence p . n is Element of D by A1; ::_thesis: verum end; definition let p be natural-valued Function; let n be set ; :: original: . redefine funcp . n -> Element of NAT ; coherence p . n is Element of NAT by ORDINAL1:def_12; end; scheme :: RECDEF_1:sch 1 RecEx{ F1() -> set , P1[ set , set , set ] } : ex f being Function st ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) provided A1: for n being Element of NAT for x being set ex y being set st P1[n,x,y] proof defpred S1[ set , set , set ] means ex O2 being Ordinal st ( O2 = \$3 & ( for X being set for n being Element of NAT st X c= Rank (the_rank_of \$2) holds ex Y being set st ( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set for n being Element of NAT st X c= Rank (the_rank_of \$2) holds ex Y being set st ( Y c= Rank O & P1[n,X,Y] ) ) holds O2 c= O ) ); A2: for n being Element of NAT for x being set ex y being set st S1[n,x,y] proof defpred S2[ set , set ] means for m being Element of NAT ex y being set st ( \$2 is Ordinal & y c= Rank (the_rank_of \$2) & P1[m,\$1,y] ); let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y] let x be set ; ::_thesis: ex y being set st S1[n,x,y] defpred S3[ Ordinal] means for X being set for n being Element of NAT st X c= Rank (the_rank_of x) holds ex Y being set st ( Y c= Rank \$1 & P1[n,X,Y] ); A3: for x9 being set st x9 in bool (Rank (the_rank_of x)) holds ex o being set st S2[x9,o] proof let x9 be set ; ::_thesis: ( x9 in bool (Rank (the_rank_of x)) implies ex o being set st S2[x9,o] ) assume x9 in bool (Rank (the_rank_of x)) ; ::_thesis: ex o being set st S2[x9,o] defpred S4[ set , set ] means ex y being set st ( \$2 is Ordinal & y c= Rank (the_rank_of \$2) & P1[\$1,x9,y] ); A4: for e being set st e in NAT holds ex u being set st S4[e,u] proof let i be set ; ::_thesis: ( i in NAT implies ex u being set st S4[i,u] ) assume i in NAT ; ::_thesis: ex u being set st S4[i,u] then reconsider i9 = i as Element of NAT ; thus ex o, y being set st ( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] ) ::_thesis: verum proof consider y being set such that A5: P1[i9,x9,y] by A1; take o = the_rank_of y; ::_thesis: ex y being set st ( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] ) take y ; ::_thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] ) thus o is Ordinal ; ::_thesis: ( y c= Rank (the_rank_of o) & P1[i,x9,y] ) the_rank_of (the_rank_of y) = the_rank_of y by CLASSES1:73; hence y c= Rank (the_rank_of o) by CLASSES1:65; ::_thesis: P1[i,x9,y] thus P1[i,x9,y] by A5; ::_thesis: verum end; end; consider h being Function such that A6: dom h = NAT and A7: for i being set st i in NAT holds S4[i,h . i] from CLASSES1:sch_1(A4); take o = sup (rng h); ::_thesis: S2[x9,o] thus for m being Element of NAT ex y being set st ( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] ) ::_thesis: verum proof let m be Element of NAT ; ::_thesis: ex y being set st ( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] ) consider y being set such that A8: h . m is Ordinal and A9: y c= Rank (the_rank_of (h . m)) and A10: P1[m,x9,y] by A7; reconsider O = h . m as Ordinal by A8; h . m in rng h by A6, FUNCT_1:def_3; then h . m in sup (rng h) by A8, ORDINAL2:19; then h . m c= o by ORDINAL1:def_2; then A11: Rank O c= Rank o by CLASSES1:37; take y ; ::_thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] ) thus o is Ordinal ; ::_thesis: ( y c= Rank (the_rank_of o) & P1[m,x9,y] ) y c= Rank O by A9, CLASSES1:73; then y c= Rank o by A11, XBOOLE_1:1; hence y c= Rank (the_rank_of o) by CLASSES1:73; ::_thesis: P1[m,x9,y] thus P1[m,x9,y] by A10; ::_thesis: verum end; end; consider f being Function such that A12: dom f = bool (Rank (the_rank_of x)) and A13: for x9 being set st x9 in bool (Rank (the_rank_of x)) holds S2[x9,f . x9] from CLASSES1:sch_1(A3); A14: ex O being Ordinal st S3[O] proof take O2 = sup (rng f); ::_thesis: S3[O2] thus for X being set for m being Element of NAT st X c= Rank (the_rank_of x) holds ex Y being set st ( Y c= Rank O2 & P1[m,X,Y] ) ::_thesis: verum proof let X be set ; ::_thesis: for m being Element of NAT st X c= Rank (the_rank_of x) holds ex Y being set st ( Y c= Rank O2 & P1[m,X,Y] ) let m be Element of NAT ; ::_thesis: ( X c= Rank (the_rank_of x) implies ex Y being set st ( Y c= Rank O2 & P1[m,X,Y] ) ) assume A15: X c= Rank (the_rank_of x) ; ::_thesis: ex Y being set st ( Y c= Rank O2 & P1[m,X,Y] ) then consider Y being set such that A16: f . X is Ordinal and A17: Y c= Rank (the_rank_of (f . X)) and A18: P1[m,X,Y] by A13; reconsider O = f . X as Ordinal by A16; f . X in rng f by A12, A15, FUNCT_1:def_3; then f . X in sup (rng f) by A16, ORDINAL2:19; then f . X c= O2 by ORDINAL1:def_2; then A19: Rank O c= Rank O2 by CLASSES1:37; take Y ; ::_thesis: ( Y c= Rank O2 & P1[m,X,Y] ) the_rank_of O = O by CLASSES1:73; hence Y c= Rank O2 by A17, A19, XBOOLE_1:1; ::_thesis: P1[m,X,Y] thus P1[m,X,Y] by A18; ::_thesis: verum end; end; consider O2 being Ordinal such that A20: ( S3[O2] & ( for O being Ordinal st S3[O] holds O2 c= O ) ) from ORDINAL1:sch_1(A14); take O2 ; ::_thesis: S1[n,x,O2] thus S1[n,x,O2] by A20; ::_thesis: verum end; A21: for n being Element of NAT for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds y1 = y2 proof let n be Element of NAT ; ::_thesis: for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds y1 = y2 let x, y1, y2 be set ; ::_thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 ) assume that A22: S1[n,x,y1] and A23: S1[n,x,y2] ; ::_thesis: y1 = y2 consider O2 being Ordinal such that A24: O2 = y2 and A25: ( ( for X being set for n being Element of NAT st X c= Rank (the_rank_of x) holds ex Y being set st ( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set for n being Element of NAT st X c= Rank (the_rank_of x) holds ex Y being set st ( Y c= Rank O & P1[n,X,Y] ) ) holds O2 c= O ) ) by A23; consider O1 being Ordinal such that A26: O1 = y1 and A27: ( ( for X being set for n being Element of NAT st X c= Rank (the_rank_of x) holds ex Y being set st ( Y c= Rank O1 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set for n being Element of NAT st X c= Rank (the_rank_of x) holds ex Y being set st ( Y c= Rank O & P1[n,X,Y] ) ) holds O1 c= O ) ) by A22; ( O1 c= O2 & O2 c= O1 ) by A27, A25; hence y1 = y2 by A26, A24, XBOOLE_0:def_10; ::_thesis: verum end; ex f being Function st ( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) proof deffunc H1( Element of NAT ) -> set = { k where k is Element of NAT : k <= \$1 } ; A28: for p, q being Function for k being Element of NAT st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Element of NAT st n < k holds ( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds p . k = q . k proof let p, q be Function; ::_thesis: for k being Element of NAT st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Element of NAT st n < k holds ( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds p . k = q . k let k be Element of NAT ; ::_thesis: ( dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Element of NAT st n < k holds ( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) implies p . k = q . k ) defpred S2[ Element of NAT ] means ( \$1 <= k implies p . \$1 = q . \$1 ); assume that dom p = H1(k) and dom q = H1(k + 1) and A29: p . 0 = q . 0 and A30: for n being Element of NAT st n < k holds ( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ; ::_thesis: p . k = q . k A31: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A32: ( n <= k implies p . n = q . n ) ; ::_thesis: S2[n + 1] assume n + 1 <= k ; ::_thesis: p . (n + 1) = q . (n + 1) then A33: n < k by NAT_1:13; then A34: S1[n,p . n,p . (n + 1)] by A30; S1[n,p . n,q . (n + 1)] by A30, A32, A33; hence p . (n + 1) = q . (n + 1) by A21, A34; ::_thesis: verum end; A35: S2[ 0 ] by A29; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A35, A31); hence p . k = q . k ; ::_thesis: verum end; A36: for n being Element of NAT ex p being Function st ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) ) proof defpred S2[ Element of NAT ] means ex p being Function st ( dom p = H1(\$1) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < \$1 holds S1[k,p . k,p . (k + 1)] ) ); A37: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) given p being Function such that dom p = H1(n) and A38: p . 0 = the_rank_of F1() and A39: for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ; ::_thesis: S2[n + 1] consider z being set such that A40: S1[n,p . n,z] by A2; defpred S3[ set , set ] means for k being Element of NAT st k = \$1 holds ( ( k <= n implies \$2 = p . k ) & ( k = n + 1 implies \$2 = z ) ); A41: for x being set st x in H1(n + 1) holds ex y being set st S3[x,y] proof let x be set ; ::_thesis: ( x in H1(n + 1) implies ex y being set st S3[x,y] ) assume x in H1(n + 1) ; ::_thesis: ex y being set st S3[x,y] then A42: ex m being Element of NAT st ( m = x & m <= n + 1 ) ; then reconsider t = x as Element of NAT ; A43: ( t <= n implies ex y being set st S3[x,y] ) proof assume A44: t <= n ; ::_thesis: ex y being set st S3[x,y] take p . x ; ::_thesis: S3[x,p . x] let k be Element of NAT ; ::_thesis: ( k = x implies ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) ) ) assume A45: k = x ; ::_thesis: ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) ) hence ( k <= n implies p . x = p . k ) ; ::_thesis: ( k = n + 1 implies p . x = z ) assume k = n + 1 ; ::_thesis: p . x = z then n + 1 <= n + 0 by A44, A45; hence p . x = z by XREAL_1:6; ::_thesis: verum end; ( t = n + 1 implies ex y being set st S3[x,y] ) proof assume A46: t = n + 1 ; ::_thesis: ex y being set st S3[x,y] take z ; ::_thesis: S3[x,z] let k be Element of NAT ; ::_thesis: ( k = x implies ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) ) ) assume A47: k = x ; ::_thesis: ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) ) thus ( k <= n implies z = p . k ) ::_thesis: ( k = n + 1 implies z = z ) proof assume k <= n ; ::_thesis: z = p . k then n + 1 <= n + 0 by A46, A47; hence z = p . k by XREAL_1:6; ::_thesis: verum end; thus ( k = n + 1 implies z = z ) ; ::_thesis: verum end; hence ex y being set st S3[x,y] by A42, A43, NAT_1:8; ::_thesis: verum end; consider q being Function such that A48: ( dom q = H1(n + 1) & ( for x being set st x in H1(n + 1) holds S3[x,q . x] ) ) from CLASSES1:sch_1(A41); take q ; ::_thesis: ( dom q = H1(n + 1) & q . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n + 1 holds S1[k,q . k,q . (k + 1)] ) ) thus dom q = H1(n + 1) by A48; ::_thesis: ( q . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n + 1 holds S1[k,q . k,q . (k + 1)] ) ) 0 in H1(n + 1) ; hence q . 0 = the_rank_of F1() by A38, A48; ::_thesis: for k being Element of NAT st k < n + 1 holds S1[k,q . k,q . (k + 1)] let k be Element of NAT ; ::_thesis: ( k < n + 1 implies S1[k,q . k,q . (k + 1)] ) assume A49: k < n + 1 ; ::_thesis: S1[k,q . k,q . (k + 1)] A50: now__::_thesis:_(_k_<>_n_implies_S1[k,q_._k,q_._(k_+_1)]_) A51: k + 1 <= n + 1 by A49, NAT_1:13; assume k <> n ; ::_thesis: S1[k,q . k,q . (k + 1)] then k + 1 <> n + 1 ; then A52: k + 1 <= n by A51, NAT_1:8; then A53: k < n by NAT_1:13; k + 1 in H1(n + 1) by A51; then A54: q . (k + 1) = p . (k + 1) by A48, A52; k in H1(n + 1) by A49; then p . k = q . k by A48, A53; hence S1[k,q . k,q . (k + 1)] by A39, A54, A53; ::_thesis: verum end; now__::_thesis:_(_k_=_n_implies_S1[k,q_._k,q_._(k_+_1)]_) assume A55: k = n ; ::_thesis: S1[k,q . k,q . (k + 1)] then k <= n + 1 by NAT_1:11; then k in H1(n + 1) ; then A56: q . k = p . k by A48, A55; k + 1 in H1(n + 1) by A55; then q . (k + 1) = z by A48, A55; hence S1[k,q . k,q . (k + 1)] by A40, A55, A56; ::_thesis: verum end; hence S1[k,q . k,q . (k + 1)] by A50; ::_thesis: verum end; A57: S2[ 0 ] proof set s = H1( 0 ) --> (the_rank_of F1()); take H1( 0 ) --> (the_rank_of F1()) ; ::_thesis: ( dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) & (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Element of NAT st k < 0 holds S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) ) thus dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) by FUNCOP_1:13; ::_thesis: ( (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Element of NAT st k < 0 holds S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) ) 0 in H1( 0 ) ; hence (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() by FUNCOP_1:7; ::_thesis: for k being Element of NAT st k < 0 holds S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] thus for k being Element of NAT st k < 0 holds S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ; ::_thesis: verum end; thus for n being Element of NAT holds S2[n] from NAT_1:sch_1(A57, A37); ::_thesis: verum end; ex f being Function st ( dom f = NAT & ( for n being Element of NAT ex p being Function st ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) ) proof defpred S2[ set , set ] means for n being Element of NAT st n = \$1 holds ex p being Function st ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & \$2 = p . n ); A58: for x being set st x in NAT holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st S2[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S2[x,y] then reconsider n = x as Element of NAT ; consider p being Function such that A59: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) ) by A36; take p . n ; ::_thesis: S2[x,p . n] let k be Element of NAT ; ::_thesis: ( k = x implies ex p being Function st ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) ) assume A60: k = x ; ::_thesis: ex p being Function st ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) take p ; ::_thesis: ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) thus ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) by A59, A60; ::_thesis: verum end; consider f being Function such that A61: ( dom f = NAT & ( for x being set st x in NAT holds S2[x,f . x] ) ) from CLASSES1:sch_1(A58); take f ; ::_thesis: ( dom f = NAT & ( for n being Element of NAT ex p being Function st ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) ) thus dom f = NAT by A61; ::_thesis: for n being Element of NAT ex p being Function st ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) let n be Element of NAT ; ::_thesis: ex p being Function st ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) consider p being Function such that A62: ( dom p = H1(n) & p . 0 = the_rank_of F1() ) and A63: for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] and A64: f . n = p . n by A61; take p ; ::_thesis: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) thus ( dom p = H1(n) & p . 0 = the_rank_of F1() ) by A62; ::_thesis: ( ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) thus for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] by A63; ::_thesis: f . n = p . n thus f . n = p . n by A64; ::_thesis: verum end; then consider f being Function such that A65: dom f = NAT and A66: for n being Element of NAT ex p being Function st ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ; take f ; ::_thesis: ( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) thus dom f = NAT by A65; ::_thesis: ( f . 0 = the_rank_of F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) ex p being Function st ( dom p = H1( 0 ) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < 0 holds S1[k,p . k,p . (k + 1)] ) & f . 0 = p . 0 ) by A66; hence f . 0 = the_rank_of F1() ; ::_thesis: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] let d be Element of NAT ; ::_thesis: S1[d,f . d,f . (d + 1)] consider p being Function such that A67: dom p = H1(d + 1) and A68: p . 0 = the_rank_of F1() and A69: for k being Element of NAT st k < d + 1 holds S1[k,p . k,p . (k + 1)] and A70: f . (d + 1) = p . (d + 1) by A66; consider q being Function such that A71: dom q = H1(d) and A72: q . 0 = the_rank_of F1() and A73: for k being Element of NAT st k < d holds S1[k,q . k,q . (k + 1)] and A74: f . d = q . d by A66; ( dom p = H1(d + 1) & dom q = H1(d) & p . 0 = q . 0 & ( for k being Element of NAT st k < d holds ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) ) proof thus dom p = H1(d + 1) by A67; ::_thesis: ( dom q = H1(d) & p . 0 = q . 0 & ( for k being Element of NAT st k < d holds ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) ) thus dom q = H1(d) by A71; ::_thesis: ( p . 0 = q . 0 & ( for k being Element of NAT st k < d holds ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) ) thus p . 0 = q . 0 by A68, A72; ::_thesis: for k being Element of NAT st k < d holds ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) let k be Element of NAT ; ::_thesis: ( k < d implies ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) assume A75: k < d ; ::_thesis: ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) hence S1[k,q . k,q . (k + 1)] by A73; ::_thesis: S1[k,p . k,p . (k + 1)] d <= d + 1 by NAT_1:11; then k < d + 1 by A75, XXREAL_0:2; hence S1[k,p . k,p . (k + 1)] by A69; ::_thesis: verum end; then p . d = q . d by A28; hence S1[d,f . d,f . (d + 1)] by A69, A70, A74, XREAL_1:29; ::_thesis: verum end; then consider g being Function such that A76: dom g = NAT and A77: g . 0 = the_rank_of F1() and A78: for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ; defpred S2[ set , set ] means ex i being Element of NAT st ( i = \$1 `2 & P1[\$1 `2 ,\$1 `1 ,\$2 `1 ] & \$2 `2 = i + 1 & ( for y being set holds ( not P1[\$1 `2 ,\$1 `1 ,y] or not the_rank_of y in the_rank_of (\$2 `1) ) ) ); A79: ( [F1(),0] `1 = F1() & [F1(),0] `2 = 0 ) ; set beta = sup (rng g); A80: for x being set st x in [:(Rank (sup (rng g))),NAT:] holds ex u being set st S2[x,u] proof let x be set ; ::_thesis: ( x in [:(Rank (sup (rng g))),NAT:] implies ex u being set st S2[x,u] ) defpred S3[ Ordinal] means ex y being set st ( y c= Rank \$1 & P1[x `2 ,x `1 ,y] ); assume x in [:(Rank (sup (rng g))),NAT:] ; ::_thesis: ex u being set st S2[x,u] then consider a, b being set such that A81: a in Rank (sup (rng g)) and A82: b in NAT and A83: x = [a,b] by ZFMISC_1:def_2; reconsider b = b as Element of NAT by A82; A84: ( x `2 = b & x `1 = a ) by A83, MCART_1:7; the_rank_of a in sup (rng g) by A81, CLASSES1:66; then consider alfa being Ordinal such that A85: alfa in rng g and A86: the_rank_of a c= alfa by ORDINAL2:21; consider k being set such that A87: k in dom g and A88: alfa = g . k by A85, FUNCT_1:def_3; reconsider k = k as Element of NAT by A76, A87; A89: S1[k,alfa,g . (k + 1)] by A78, A88; then reconsider O2 = g . (k + 1) as Ordinal ; a c= Rank alfa by A86, CLASSES1:65; then a c= Rank (the_rank_of alfa) by CLASSES1:73; then ex y being set st ( y c= Rank O2 & P1[x `2 ,x `1 ,y] ) by A89, A84; then A90: ex O being Ordinal st S3[O] ; consider O being Ordinal such that A91: S3[O] and A92: for O9 being Ordinal st S3[O9] holds O c= O9 from ORDINAL1:sch_1(A90); consider Y being set such that A93: Y c= Rank O and A94: P1[b,a,Y] by A84, A91; A95: the_rank_of Y c= O by A93, CLASSES1:65; take u = [Y,(b + 1)]; ::_thesis: S2[x,u] take i = b; ::_thesis: ( i = x `2 & P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds ( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) ) thus i = x `2 by A83, MCART_1:7; ::_thesis: ( P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds ( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) ) thus P1[x `2 ,x `1 ,u `1 ] by A84, A94, MCART_1:7; ::_thesis: ( u `2 = i + 1 & ( for y being set holds ( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) ) thus u `2 = i + 1 by MCART_1:7; ::_thesis: for y being set holds ( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) given y being set such that A96: P1[x `2 ,x `1 ,y] and A97: the_rank_of y in the_rank_of (u `1) ; ::_thesis: contradiction A98: y c= Rank (the_rank_of y) by CLASSES1:def_8; the_rank_of y in the_rank_of Y by A97, MCART_1:7; hence contradiction by A92, A96, A95, A98, ORDINAL1:5; ::_thesis: verum end; consider F being Function such that dom F = [:(Rank (sup (rng g))),NAT:] and A99: for x being set st x in [:(Rank (sup (rng g))),NAT:] holds S2[x,F . x] from CLASSES1:sch_1(A80); deffunc H1( Nat, set ) -> set = (F . [\$2,\$1]) `1 ; consider f being Function such that A100: dom f = NAT and A101: f . 0 = F1() and A102: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_11(); defpred S3[ Element of NAT ] means the_rank_of (f . \$1) in sup (rng g); g . 0 in rng g by A76, FUNCT_1:def_3; then A103: S3[ 0 ] by A77, A101, ORDINAL2:19; A104: for n being Element of NAT st S3[n] holds S3[n + 1] proof let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] ) assume A105: the_rank_of (f . n) in sup (rng g) ; ::_thesis: S3[n + 1] then consider o1 being Ordinal such that A106: o1 in rng g and A107: the_rank_of (f . n) c= o1 by ORDINAL2:21; f . n in Rank (sup (rng g)) by A105, CLASSES1:66; then A108: [(f . n),n] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87; consider m being set such that A109: m in dom g and A110: g . m = o1 by A106, FUNCT_1:def_3; reconsider m = m as Element of NAT by A76, A109; consider o2 being Ordinal such that A111: o2 = g . (m + 1) and A112: for X being set for n being Element of NAT st X c= Rank (the_rank_of (g . m)) holds ex Y being set st ( Y c= Rank o2 & P1[n,X,Y] ) and for o being Ordinal st ( for X being set for n being Element of NAT st X c= Rank (the_rank_of (g . m)) holds ex Y being set st ( Y c= Rank o & P1[n,X,Y] ) ) holds o2 c= o by A78; the_rank_of (f . n) c= the_rank_of (g . m) by A107, A110, CLASSES1:73; then f . n c= Rank (the_rank_of (g . m)) by CLASSES1:65; then consider YY being set such that A113: YY c= Rank o2 and A114: P1[n,f . n,YY] by A112; A115: the_rank_of YY c= o2 by A113, CLASSES1:65; ( [(f . n),n] `1 = f . n & [(f . n),n] `2 = n ) ; then ex i being Element of NAT st ( i = n & P1[n,f . n,(F . [(f . n),n]) `1 ] & (F . [(f . n),n]) `2 = i + 1 & ( for y being set holds ( not P1[n,f . n,y] or not the_rank_of y in the_rank_of ((F . [(f . n),n]) `1) ) ) ) by A99, A108; then A116: the_rank_of ((F . [(f . n),n]) `1) c= the_rank_of YY by A114, ORDINAL1:16; g . (m + 1) in rng g by A76, FUNCT_1:def_3; then A117: o2 in sup (rng g) by A111, ORDINAL2:19; f . (n + 1) = (F . [(f . n),n]) `1 by A102; hence S3[n + 1] by A116, A115, A117, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum end; A118: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A103, A104); defpred S4[ Element of NAT ] means P1[\$1,f . \$1,f . (\$1 + 1)]; A119: for n being Element of NAT st S4[n] holds S4[n + 1] proof let n be Element of NAT ; ::_thesis: ( S4[n] implies S4[n + 1] ) assume P1[n,f . n,f . (n + 1)] ; ::_thesis: S4[n + 1] the_rank_of (f . (n + 1)) in sup (rng g) by A118; then f . (n + 1) in Rank (sup (rng g)) by CLASSES1:66; then A120: [(f . (n + 1)),(n + 1)] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87; ( [(f . (n + 1)),(n + 1)] `1 = f . (n + 1) & [(f . (n + 1)),(n + 1)] `2 = n + 1 ) ; then ex i being Element of NAT st ( i = n + 1 & P1[n + 1,f . (n + 1),(F . [(f . (n + 1)),(n + 1)]) `1 ] & (F . [(f . (n + 1)),(n + 1)]) `2 = i + 1 & ( for y being set holds ( not P1[n + 1,f . (n + 1),y] or not the_rank_of y in the_rank_of ((F . [(f . (n + 1)),(n + 1)]) `1) ) ) ) by A99, A120; hence S4[n + 1] by A102; ::_thesis: verum end; take f ; ::_thesis: ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) thus dom f = NAT by A100; ::_thesis: ( f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) thus f . 0 = F1() by A101; ::_thesis: for n being Element of NAT holds P1[n,f . n,f . (n + 1)] F1() in Rank (sup (rng g)) by A101, A103, CLASSES1:66; then [F1(),0] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87; then ex i being Element of NAT st ( i = [F1(),0] `2 & P1[ 0 ,F1(),(F . [F1(),0]) `1 ] & (F . [F1(),0]) `2 = i + 1 & ( for y being set holds ( not P1[ 0 ,F1(),y] or not the_rank_of y in the_rank_of ((F . [F1(),0]) `1) ) ) ) by A99, A79; then A121: S4[ 0 ] by A101, A102; thus for n being Element of NAT holds S4[n] from NAT_1:sch_1(A121, A119); ::_thesis: verum end; scheme :: RECDEF_1:sch 2 RecExD{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ] } : ex f being Function of NAT,F1() st ( f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) provided A1: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st P1[n,x,y] proof defpred S1[ Element of NAT , set , set ] means P1[\$1,\$2,\$3]; A2: for x being Element of NAT for y being Element of F1() ex z being Element of F1() st S1[x,y,z] by A1; consider f being Function of [:NAT,F1():],F1() such that A3: for x being Element of NAT for y being Element of F1() holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A2); defpred S2[ FinSequence] means ( \$1 . 1 = F2() & ( for n being Element of NAT st n + 2 <= len \$1 holds \$1 . (n + 2) = f . [n,(\$1 . (n + 1))] ) ); consider X being set such that A4: for x being set holds ( x in X iff ex p being FinSequence st ( p in F1() * & S2[p] & x = p ) ) from FINSEQ_1:sch_4(); set Y = union X; A5: for x being set st x in X holds x in F1() * proof let x be set ; ::_thesis: ( x in X implies x in F1() * ) assume x in X ; ::_thesis: x in F1() * then ex p being FinSequence st ( p in F1() * & p . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p holds p . (n + 2) = f . [n,(p . (n + 1))] ) & x = p ) by A4; hence x in F1() * ; ::_thesis: verum end; A6: for p, q being FinSequence st p in X & q in X & len p <= len q holds p c= q proof let p, q be FinSequence; ::_thesis: ( p in X & q in X & len p <= len q implies p c= q ) assume that A7: p in X and A8: q in X and A9: len p <= len q ; ::_thesis: p c= q A10: ex q9 being FinSequence st ( q9 in F1() * & q9 . 1 = F2() & ( for n being Element of NAT st n + 2 <= len q9 holds q9 . (n + 2) = f . [n,(q9 . (n + 1))] ) & q = q9 ) by A4, A8; A11: ex p9 being FinSequence st ( p9 in F1() * & p9 . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p9 holds p9 . (n + 2) = f . [n,(p9 . (n + 1))] ) & p = p9 ) by A4, A7; A12: for n being Element of NAT st 1 <= n & n <= len p holds p . n = q . n proof defpred S3[ Nat] means ( 1 <= \$1 & \$1 <= len p & p . \$1 <> q . \$1 ); assume ex n being Element of NAT st S3[n] ; ::_thesis: contradiction then A13: ex n being Nat st S3[n] ; consider k being Nat such that A14: ( S3[k] & ( for n being Nat st S3[n] holds k <= n ) ) from NAT_1:sch_5(A13); k = 1 proof 0 <> k by A14; then consider n being Nat such that A15: k = n + 1 by NAT_1:6; n + 0 <= n + 1 by XREAL_1:7; then A16: n <= len p by A14, A15, XXREAL_0:2; A17: n + 0 < n + 1 by XREAL_1:6; assume A18: k <> 1 ; ::_thesis: contradiction then 1 < n + 1 by A14, A15, XXREAL_0:1; then A19: 1 <= n by NAT_1:13; n <> 0 by A18, A15; then consider m being Nat such that A20: n = m + 1 by NAT_1:6; reconsider m = m as Element of NAT by ORDINAL1:def_12; A21: m + 2 <= len q by A9, A14, A15, A20, XXREAL_0:2; p . k = p . (m + (1 + 1)) by A15, A20 .= f . [m,(p . n)] by A11, A14, A15, A20 .= f . [m,(q . (m + 1))] by A14, A15, A19, A16, A17, A20 .= q . k by A10, A15, A20, A21 ; hence contradiction by A14; ::_thesis: verum end; hence contradiction by A11, A10, A14; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_p_holds_ x_in_q let x be set ; ::_thesis: ( x in p implies x in q ) assume x in p ; ::_thesis: x in q then consider n being Nat such that A22: n in dom p and A23: x = [n,(p . n)] by FINSEQ_1:12; A24: n in Seg (len p) by A22, FINSEQ_1:def_3; then A25: 1 <= n by FINSEQ_1:1; A26: n <= len p by A24, FINSEQ_1:1; then n <= len q by A9, XXREAL_0:2; then n in Seg (len q) by A25, FINSEQ_1:1; then A27: n in dom q by FINSEQ_1:def_3; x = [n,(q . n)] by A12, A22, A23, A25, A26; hence x in q by A27, FUNCT_1:1; ::_thesis: verum end; hence p c= q by TARSKI:def_3; ::_thesis: verum end; ex f being Function st f = union X proof defpred S3[ set , set ] means [\$1,\$2] in union X; A28: for x, y, z being set st S3[x,y] & S3[x,z] holds y = z proof let x, y, z be set ; ::_thesis: ( S3[x,y] & S3[x,z] implies y = z ) assume that A29: [x,y] in union X and A30: [x,z] in union X ; ::_thesis: y = z consider Z2 being set such that A31: [x,z] in Z2 and A32: Z2 in X by A30, TARSKI:def_4; Z2 in F1() * by A5, A32; then reconsider q = Z2 as FinSequence of F1() by FINSEQ_1:def_11; consider Z1 being set such that A33: [x,y] in Z1 and A34: Z1 in X by A29, TARSKI:def_4; Z1 in F1() * by A5, A34; then reconsider p = Z1 as FinSequence of F1() by FINSEQ_1:def_11; A35: now__::_thesis:_(_len_q_<=_len_p_implies_y_=_z_) assume len q <= len p ; ::_thesis: y = z then A36: q c= Z1 by A6, A34, A32; [x,y] in p by A33; hence y = z by A31, A36, FUNCT_1:def_1; ::_thesis: verum end; now__::_thesis:_(_len_p_<=_len_q_implies_y_=_z_) assume len p <= len q ; ::_thesis: y = z then p c= Z2 by A6, A34, A32; then [x,y] in q by A33; hence y = z by A31, FUNCT_1:def_1; ::_thesis: verum end; hence y = z by A35; ::_thesis: verum end; consider h being Function such that A37: for x, y being set holds ( [x,y] in h iff ( x in NAT & S3[x,y] ) ) from FUNCT_1:sch_1(A28); take h ; ::_thesis: h = union X A38: for x, y being set holds ( [x,y] in h iff [x,y] in union X ) proof let x, y be set ; ::_thesis: ( [x,y] in h iff [x,y] in union X ) thus ( [x,y] in h implies [x,y] in union X ) by A37; ::_thesis: ( [x,y] in union X implies [x,y] in h ) thus ( [x,y] in union X implies [x,y] in h ) ::_thesis: verum proof assume A39: [x,y] in union X ; ::_thesis: [x,y] in h then consider Z being set such that A40: [x,y] in Z and A41: Z in X by TARSKI:def_4; Z in F1() * by A5, A41; then reconsider p = Z as FinSequence of F1() by FINSEQ_1:def_11; x in dom p by A40, XTUPLE_0:def_12; hence [x,y] in h by A37, A39; ::_thesis: verum end; end; for x being set holds ( x in h iff x in union X ) proof let x be set ; ::_thesis: ( x in h iff x in union X ) thus ( x in h implies x in union X ) ::_thesis: ( x in union X implies x in h ) proof assume A42: x in h ; ::_thesis: x in union X then ex y, z being set st [y,z] = x by RELAT_1:def_1; hence x in union X by A38, A42; ::_thesis: verum end; assume A43: x in union X ; ::_thesis: x in h then consider Z being set such that A44: x in Z and A45: Z in X by TARSKI:def_4; Z in F1() * by A5, A45; then reconsider p = Z as FinSequence of F1() by FINSEQ_1:def_11; x in p by A44; then ex y, z being set st [y,z] = x by RELAT_1:def_1; hence x in h by A38, A43; ::_thesis: verum end; hence h = union X by TARSKI:1; ::_thesis: verum end; then consider g being Function such that A46: g = union X ; A47: for x being set st x in rng g holds x in F1() proof let x be set ; ::_thesis: ( x in rng g implies x in F1() ) assume x in rng g ; ::_thesis: x in F1() then consider y being set such that A48: ( y in dom g & x = g . y ) by FUNCT_1:def_3; [y,x] in union X by A46, A48, FUNCT_1:1; then consider Z being set such that A49: [y,x] in Z and A50: Z in X by TARSKI:def_4; Z in F1() * by A5, A50; then reconsider p = Z as FinSequence of F1() by FINSEQ_1:def_11; ( y in dom p & x = p . y ) by A49, FUNCT_1:1; then A51: x in rng p by FUNCT_1:def_3; rng p c= F1() by FINSEQ_1:def_4; hence x in F1() by A51; ::_thesis: verum end; then rng g c= F1() by TARSKI:def_3; then reconsider h = g as Function of (dom g),F1() by FUNCT_2:2; A52: for n being Element of NAT holds n + 1 in dom h proof defpred S3[ Element of NAT ] means \$1 + 1 in dom h; A53: for n being Element of NAT st n + 2 <= len <*F2()*> holds <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] proof let n be Element of NAT ; ::_thesis: ( n + 2 <= len <*F2()*> implies <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] ) assume n + 2 <= len <*F2()*> ; ::_thesis: <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] then n + 2 <= 1 by FINSEQ_1:39; then n + (1 + 1) <= n + 1 by NAT_1:12; hence <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] by XREAL_1:6; ::_thesis: verum end; ( <*F2()*> . 1 = F2() & <*F2()*> in F1() * ) by FINSEQ_1:def_8, FINSEQ_1:def_11; then <*F2()*> in X by A4, A53; then A54: {[1,F2()]} in X by FINSEQ_1:37; A55: for k being Element of NAT st S3[k] holds S3[k + 1] proof let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] ) assume k + 1 in dom h ; ::_thesis: S3[k + 1] then [(k + 1),(h . (k + 1))] in union X by A46, FUNCT_1:1; then consider Z being set such that A56: [(k + 1),(h . (k + 1))] in Z and A57: Z in X by TARSKI:def_4; Z in F1() * by A5, A57; then reconsider Z = Z as FinSequence of F1() by FINSEQ_1:def_11; A58: ( k + 1 = len Z implies S3[k + 1] ) proof set p = Z ^ <*(f . [k,(Z . (k + 1))])*>; A59: 1 <= (k + 1) + 1 by NAT_1:12; assume A60: k + 1 = len Z ; ::_thesis: S3[k + 1] then 1 <= len Z by NAT_1:12; then 1 in Seg (len Z) by FINSEQ_1:1; then A61: 1 in dom Z by FINSEQ_1:def_3; A62: for n being Element of NAT st n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) holds (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] proof let n be Element of NAT ; ::_thesis: ( n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] ) assume n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) ; ::_thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] then A63: n + 2 <= (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22; then A64: n + 2 <= (len Z) + 1 by FINSEQ_1:40; A65: ( n + 2 <> (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] ) proof (n + 1) + 1 <= (len Z) + 1 by A63, FINSEQ_1:40; then ( 1 <= n + 1 & n + 1 <= len Z ) by NAT_1:12, XREAL_1:6; then n + 1 in Seg (len Z) by FINSEQ_1:1; then A66: n + 1 in dom Z by FINSEQ_1:def_3; A67: 1 <= n + (1 + 1) by NAT_1:12; assume A68: n + 2 <> (len Z) + 1 ; ::_thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] then n + 2 <= len Z by A64, NAT_1:8; then n + 2 in Seg (len Z) by A67, FINSEQ_1:1; then A69: n + 2 in dom Z by FINSEQ_1:def_3; ex q being FinSequence st ( q in F1() * & q . 1 = F2() & ( for n being Element of NAT st n + 2 <= len q holds q . (n + 2) = f . [n,(q . (n + 1))] ) & Z = q ) by A4, A57; then Z . (n + 2) = f . [n,(Z . (n + 1))] by A64, A68, NAT_1:8; then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,(Z . (n + 1))] by A69, FINSEQ_1:def_7; hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A66, FINSEQ_1:def_7; ::_thesis: verum end; ( n + 2 = (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] ) proof (n + 1) + 1 <= (len Z) + 1 by A63, FINSEQ_1:40; then ( 1 <= n + 1 & n + 1 <= len Z ) by NAT_1:12, XREAL_1:6; then n + 1 in Seg (len Z) by FINSEQ_1:1; then A70: n + 1 in dom Z by FINSEQ_1:def_3; assume A71: n + 2 = (len Z) + 1 ; ::_thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = <*(f . [k,(Z . (k + 1))])*> . ((n + 2) - ((n + 2) - 1)) by A63, FINSEQ_1:23 .= f . [n,(Z . (n + 1))] by A60, A71, FINSEQ_1:40 ; hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A70, FINSEQ_1:def_7; ::_thesis: verum end; hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A65; ::_thesis: verum end; A72: Z ^ <*(f . [k,(Z . (k + 1))])*> in F1() * proof 1 <= k + 1 by NAT_1:12; then k + 1 in Seg (len Z) by A60, FINSEQ_1:1; then k + 1 in dom Z by FINSEQ_1:def_3; then A73: Z . (k + 1) in rng Z by FUNCT_1:def_3; rng Z c= F1() by FINSEQ_1:def_4; then reconsider z = Z . (k + 1) as Element of F1() by A73; reconsider n = k as Element of NAT ; Z ^ <*(f . [k,(Z . (k + 1))])*> = Z ^ <*(f . [n,z])*> ; hence Z ^ <*(f . [k,(Z . (k + 1))])*> in F1() * by FINSEQ_1:def_11; ::_thesis: verum end; len (Z ^ <*(f . [k,(Z . (k + 1))])*>) = (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22 .= (k + 1) + 1 by A60, FINSEQ_1:39 ; then (k + 1) + 1 in Seg (len (Z ^ <*(f . [k,(Z . (k + 1))])*>)) by A59, FINSEQ_1:1; then (k + 1) + 1 in dom (Z ^ <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:def_3; then A74: [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in Z ^ <*(f . [k,(Z . (k + 1))])*> by FUNCT_1:1; ex p being FinSequence st ( p in F1() * & p . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p holds p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A57; then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . 1 = F2() by A61, FINSEQ_1:def_7; then Z ^ <*(f . [k,(Z . (k + 1))])*> in X by A4, A72, A62; then [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in h by A46, A74, TARSKI:def_4; hence S3[k + 1] by FUNCT_1:1; ::_thesis: verum end; ( k + 1 <> len Z implies S3[k + 1] ) proof k + 1 in dom Z by A56, FUNCT_1:1; then k + 1 in Seg (len Z) by FINSEQ_1:def_3; then A75: k + 1 <= len Z by FINSEQ_1:1; assume k + 1 <> len Z ; ::_thesis: S3[k + 1] then k + 1 < len Z by A75, XXREAL_0:1; then A76: (k + 1) + 1 <= len Z by NAT_1:13; 1 <= (k + 1) + 1 by NAT_1:12; then (k + 1) + 1 in Seg (len Z) by A76, FINSEQ_1:1; then (k + 1) + 1 in dom Z by FINSEQ_1:def_3; then [((k + 1) + 1),(Z . ((k + 1) + 1))] in Z by FUNCT_1:1; then [((k + 1) + 1),(Z . ((k + 1) + 1))] in h by A46, A57, TARSKI:def_4; hence S3[k + 1] by FUNCT_1:1; ::_thesis: verum end; hence S3[k + 1] by A58; ::_thesis: verum end; [1,F2()] in {[1,F2()]} by TARSKI:def_1; then [1,F2()] in h by A46, A54, TARSKI:def_4; then A77: S3[ 0 ] by FUNCT_1:1; thus for k being Element of NAT holds S3[k] from NAT_1:sch_1(A77, A55); ::_thesis: verum end; A78: for n being Element of NAT holds h . (n + 2) = f . [n,(h . (n + 1))] proof let n be Element of NAT ; ::_thesis: h . (n + 2) = f . [n,(h . (n + 1))] (n + 1) + 1 in dom h by A52; then [(n + 2),(h . (n + 2))] in h by FUNCT_1:def_2; then consider Z being set such that A79: [(n + 2),(h . (n + 2))] in Z and A80: Z in X by A46, TARSKI:def_4; A81: ex p being FinSequence st ( p in F1() * & p . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p holds p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A80; Z in F1() * by A5, A80; then reconsider Z = Z as FinSequence of F1() by FINSEQ_1:def_11; n + 2 in dom Z by A79, FUNCT_1:1; then n + 2 in Seg (len Z) by FINSEQ_1:def_3; then A82: n + 2 <= len Z by FINSEQ_1:1; n + 1 <= n + 2 by XREAL_1:7; then ( 1 <= n + 1 & n + 1 <= len Z ) by A82, NAT_1:12, XXREAL_0:2; then n + 1 in Seg (len Z) by FINSEQ_1:1; then n + 1 in dom Z by FINSEQ_1:def_3; then [(n + 1),(Z . (n + 1))] in Z by FUNCT_1:1; then A83: [(n + 1),(Z . (n + 1))] in h by A46, A80, TARSKI:def_4; thus h . (n + 2) = Z . (n + 2) by A79, FUNCT_1:1 .= f . [n,(Z . (n + 1))] by A81, A82 .= f . [n,(h . (n + 1))] by A83, FUNCT_1:1 ; ::_thesis: verum end; ex g being Function of NAT,F1() st for n being Element of NAT holds g . n = h . (n + 1) proof ex g being Function st ( dom g = NAT & ( for n being Element of NAT holds g . n = h . (n + 1) ) ) proof defpred S3[ set , set ] means ex n being Element of NAT st ( n = \$1 & \$2 = h . (n + 1) ); A84: for x being set st x in NAT holds ex y being set st S3[x,y] proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st S3[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S3[x,y] then reconsider n = x as Element of NAT ; take h . (n + 1) ; ::_thesis: S3[x,h . (n + 1)] take n ; ::_thesis: ( n = x & h . (n + 1) = h . (n + 1) ) thus ( n = x & h . (n + 1) = h . (n + 1) ) ; ::_thesis: verum end; consider g being Function such that A85: ( dom g = NAT & ( for x being set st x in NAT holds S3[x,g . x] ) ) from CLASSES1:sch_1(A84); take g ; ::_thesis: ( dom g = NAT & ( for n being Element of NAT holds g . n = h . (n + 1) ) ) thus dom g = NAT by A85; ::_thesis: for n being Element of NAT holds g . n = h . (n + 1) thus for n being Element of NAT holds g . n = h . (n + 1) ::_thesis: verum proof let n be Element of NAT ; ::_thesis: g . n = h . (n + 1) ex m being Element of NAT st ( m = n & g . n = h . (m + 1) ) by A85; hence g . n = h . (n + 1) ; ::_thesis: verum end; end; then consider g being Function such that A86: dom g = NAT and A87: for n being Element of NAT holds g . n = h . (n + 1) ; rng g c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in F1() ) assume x in rng g ; ::_thesis: x in F1() then consider y being set such that A88: y in dom g and A89: x = g . y by FUNCT_1:def_3; reconsider k = y as Element of NAT by A86, A88; k + 1 in dom h by A52; then A90: h . (k + 1) in rng h by FUNCT_1:def_3; x = h . (k + 1) by A87, A89; hence x in F1() by A47, A90; ::_thesis: verum end; then reconsider g = g as Function of NAT,F1() by A86, FUNCT_2:2; take g ; ::_thesis: for n being Element of NAT holds g . n = h . (n + 1) thus for n being Element of NAT holds g . n = h . (n + 1) by A87; ::_thesis: verum end; then consider g being Function of NAT,F1() such that A91: for n being Element of NAT holds g . n = h . (n + 1) ; A92: for n being Element of NAT st n + 2 <= len <*F2()*> holds <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] proof let n be Element of NAT ; ::_thesis: ( n + 2 <= len <*F2()*> implies <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] ) assume n + 2 <= len <*F2()*> ; ::_thesis: <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] then (n + 1) + 1 <= 0 + 1 by FINSEQ_1:39; then n + 1 <= 0 by XREAL_1:6; then n + 1 <= 0 + n ; hence <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] by XREAL_1:6; ::_thesis: verum end; ( <*F2()*> in F1() * & <*F2()*> . 1 = F2() ) by FINSEQ_1:def_8, FINSEQ_1:def_11; then <*F2()*> in X by A4, A92; then A93: {[1,F2()]} in X by FINSEQ_1:37; take g ; ::_thesis: ( g . 0 = F2() & ( for n being Element of NAT holds P1[n,g . n,g . (n + 1)] ) ) [1,F2()] in {[1,F2()]} by TARSKI:def_1; then [1,F2()] in h by A46, A93, TARSKI:def_4; then F2() = h . (0 + 1) by FUNCT_1:1 .= g . 0 by A91 ; hence g . 0 = F2() ; ::_thesis: for n being Element of NAT holds P1[n,g . n,g . (n + 1)] let n be Element of NAT ; ::_thesis: P1[n,g . n,g . (n + 1)] A94: h . (n + (1 + 1)) = f . (n,(h . (n + 1))) by A78; P1[n,g . n,f . (n,(g . n))] by A3; then P1[n,g . n,h . ((n + 1) + 1)] by A91, A94; hence P1[n,g . n,g . (n + 1)] by A91; ::_thesis: verum end; scheme :: RECDEF_1:sch 3 FinRecEx{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } : ex p being FinSequence st ( len p = F2() & ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,p . n,p . (n + 1)] ) ) provided A1: for n being Element of NAT st 1 <= n & n < F2() holds for x being set ex y being set st P1[n,x,y] proof defpred S1[ Element of NAT , set , set ] means ( ( \$1 < F2() - 1 implies P1[\$1 + 1,\$2,\$3] ) & ( not \$1 < F2() - 1 implies \$3 = 0 ) ); A2: for n being Element of NAT for x being set ex y being set st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y] let x be set ; ::_thesis: ex y being set st S1[n,x,y] ( n < F2() - 1 implies ex y being set st S1[n,x,y] ) proof assume A3: n < F2() - 1 ; ::_thesis: ex y being set st S1[n,x,y] then n + 1 < F2() by XREAL_1:20; then consider y being set such that A4: P1[n + 1,x,y] by A1, NAT_1:11; take y ; ::_thesis: S1[n,x,y] thus ( n < F2() - 1 implies P1[n + 1,x,y] ) by A4; ::_thesis: ( not n < F2() - 1 implies y = 0 ) thus ( not n < F2() - 1 implies y = 0 ) by A3; ::_thesis: verum end; hence ex y being set st S1[n,x,y] ; ::_thesis: verum end; consider f being Function such that A5: ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_1(A2); defpred S2[ set , set ] means for r being Real st r = \$1 holds \$2 = f . (r - 1); A6: for x being set st x in REAL holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in REAL implies ex y being set st S2[x,y] ) assume x in REAL ; ::_thesis: ex y being set st S2[x,y] then reconsider r = x as Real ; take f . (r - 1) ; ::_thesis: S2[x,f . (r - 1)] thus S2[x,f . (r - 1)] ; ::_thesis: verum end; consider g being Function such that A7: ( dom g = REAL & ( for x being set st x in REAL holds S2[x,g . x] ) ) from CLASSES1:sch_1(A6); A8: dom (g | (Seg F2())) = Seg F2() by A7, RELAT_1:62, XBOOLE_1:1; then reconsider p = g | (Seg F2()) as FinSequence by FINSEQ_1:def_2; take p ; ::_thesis: ( len p = F2() & ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,p . n,p . (n + 1)] ) ) F2() in NAT by ORDINAL1:def_12; hence len p = F2() by A8, FINSEQ_1:def_3; ::_thesis: ( ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,p . n,p . (n + 1)] ) ) ( not F2() <> 0 or p . 1 = F1() or F2() = 0 ) proof assume F2() <> 0 ; ::_thesis: ( p . 1 = F1() or F2() = 0 ) then consider k being Nat such that A9: F2() = k + 1 by NAT_1:6; 0 + 1 <= k + 1 by XREAL_1:7; then 1 in Seg F2() by A9, FINSEQ_1:1; then p . 1 = g . 1 by FUNCT_1:49 .= f . (1 - 1) by A7 .= F1() by A5 ; hence ( p . 1 = F1() or F2() = 0 ) ; ::_thesis: verum end; hence ( p . 1 = F1() or F2() = 0 ) ; ::_thesis: for n being Element of NAT st 1 <= n & n < F2() holds P1[n,p . n,p . (n + 1)] let n be Element of NAT ; ::_thesis: ( 1 <= n & n < F2() implies P1[n,p . n,p . (n + 1)] ) assume that A10: 1 <= n and A11: n < F2() ; ::_thesis: P1[n,p . n,p . (n + 1)] 0 <> n by A10; then consider k being Nat such that A12: n = k + 1 by NAT_1:6; A13: for n being Element of NAT st n < F2() holds p . (n + 1) = f . n proof let n be Element of NAT ; ::_thesis: ( n < F2() implies p . (n + 1) = f . n ) assume n < F2() ; ::_thesis: p . (n + 1) = f . n then ( 1 <= n + 1 & n + 1 <= F2() ) by NAT_1:11, NAT_1:13; then A14: n + 1 in Seg F2() by FINSEQ_1:1; g . (n + 1) = f . ((n + 1) - 1) by A7 .= f . n ; hence p . (n + 1) = f . n by A14, FUNCT_1:49; ::_thesis: verum end; reconsider k = k as Element of NAT by ORDINAL1:def_12; k <= k + 1 by NAT_1:11; then A15: k < F2() by A11, A12, XXREAL_0:2; k < F2() - 1 by A11, A12, XREAL_1:20; then P1[k + 1,f . k,f . (k + 1)] by A5; then P1[k + 1,f . k,p . ((k + 1) + 1)] by A13, A11, A12; hence P1[n,p . n,p . (n + 1)] by A13, A12, A15; ::_thesis: verum end; scheme :: RECDEF_1:sch 4 FinRecExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } : ex p being FinSequence of F1() st ( len p = F3() & ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,p . n,p . (n + 1)] ) ) provided A1: for n being Element of NAT st 1 <= n & n < F3() holds for x being Element of F1() ex y being Element of F1() st P1[n,x,y] proof set 00 = the Element of F1(); defpred S1[ Element of NAT , set , set ] means ( ( \$1 < F3() - 1 implies P1[\$1 + 1,\$2,\$3] ) & ( not \$1 < F3() - 1 implies \$3 = the Element of F1() ) ); A2: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y] let x be Element of F1(); ::_thesis: ex y being Element of F1() st S1[n,x,y] ( n < F3() - 1 implies ex y being Element of F1() st S1[n,x,y] ) proof assume A3: n < F3() - 1 ; ::_thesis: ex y being Element of F1() st S1[n,x,y] then n + 1 < F3() by XREAL_1:20; then consider y being Element of F1() such that A4: P1[n + 1,x,y] by A1, NAT_1:11; take y ; ::_thesis: S1[n,x,y] thus ( n < F3() - 1 implies P1[n + 1,x,y] ) by A4; ::_thesis: ( not n < F3() - 1 implies y = the Element of F1() ) thus ( not n < F3() - 1 implies y = the Element of F1() ) by A3; ::_thesis: verum end; hence ex y being Element of F1() st S1[n,x,y] ; ::_thesis: verum end; consider f being Function of NAT,F1() such that A5: ( f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A2); defpred S2[ set , set ] means for r being Real st r = \$1 holds \$2 = f . (r - 1); A6: for x being set st x in REAL holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in REAL implies ex y being set st S2[x,y] ) assume x in REAL ; ::_thesis: ex y being set st S2[x,y] then reconsider r = x as Real ; take f . (r - 1) ; ::_thesis: S2[x,f . (r - 1)] thus S2[x,f . (r - 1)] ; ::_thesis: verum end; consider g being Function such that A7: ( dom g = REAL & ( for x being set st x in REAL holds S2[x,g . x] ) ) from CLASSES1:sch_1(A6); A8: dom (g | (Seg F3())) = Seg F3() by A7, RELAT_1:62, XBOOLE_1:1; then reconsider p = g | (Seg F3()) as FinSequence by FINSEQ_1:def_2; rng p c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in F1() ) assume x in rng p ; ::_thesis: x in F1() then consider y being set such that A9: y in dom p and A10: x = p . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A9; A11: f . (y - 1) in F1() proof y <> 0 by A8, A9, FINSEQ_1:1; then consider k being Nat such that A12: y = k + 1 by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; f . k in F1() ; hence f . (y - 1) in F1() by A12; ::_thesis: verum end; p . y = g . y by A9, FUNCT_1:47; hence x in F1() by A7, A10, A11; ::_thesis: verum end; then reconsider p = p as FinSequence of F1() by FINSEQ_1:def_4; take p ; ::_thesis: ( len p = F3() & ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,p . n,p . (n + 1)] ) ) F3() in NAT by ORDINAL1:def_12; hence len p = F3() by A8, FINSEQ_1:def_3; ::_thesis: ( ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,p . n,p . (n + 1)] ) ) ( not F3() <> 0 or p . 1 = F2() or F3() = 0 ) proof assume F3() <> 0 ; ::_thesis: ( p . 1 = F2() or F3() = 0 ) then consider k being Nat such that A13: F3() = k + 1 by NAT_1:6; 0 + 1 <= k + 1 by XREAL_1:7; then 1 in Seg F3() by A13, FINSEQ_1:1; then p . 1 = g . 1 by FUNCT_1:49 .= f . (1 - 1) by A7 .= F2() by A5 ; hence ( p . 1 = F2() or F3() = 0 ) ; ::_thesis: verum end; hence ( p . 1 = F2() or F3() = 0 ) ; ::_thesis: for n being Element of NAT st 1 <= n & n < F3() holds P1[n,p . n,p . (n + 1)] let n be Element of NAT ; ::_thesis: ( 1 <= n & n < F3() implies P1[n,p . n,p . (n + 1)] ) assume that A14: 1 <= n and A15: n < F3() ; ::_thesis: P1[n,p . n,p . (n + 1)] 0 <> n by A14; then consider k being Nat such that A16: n = k + 1 by NAT_1:6; A17: for n being Element of NAT st n < F3() holds p . (n + 1) = f . n proof let n be Element of NAT ; ::_thesis: ( n < F3() implies p . (n + 1) = f . n ) assume n < F3() ; ::_thesis: p . (n + 1) = f . n then ( 1 <= n + 1 & n + 1 <= F3() ) by NAT_1:11, NAT_1:13; then A18: n + 1 in Seg F3() by FINSEQ_1:1; g . (n + 1) = f . ((n + 1) - 1) by A7 .= f . n ; hence p . (n + 1) = f . n by A18, FUNCT_1:49; ::_thesis: verum end; reconsider k = k as Element of NAT by ORDINAL1:def_12; k <= k + 1 by NAT_1:11; then A19: k < F3() by A15, A16, XXREAL_0:2; k < F3() - 1 by A15, A16, XREAL_1:20; then P1[k + 1,f . k,f . (k + 1)] by A5; then P1[k + 1,f . k,p . ((k + 1) + 1)] by A17, A15, A16; hence P1[n,p . n,p . (n + 1)] by A17, A16, A19; ::_thesis: verum end; scheme :: RECDEF_1:sch 5 SeqBinOpEx{ F1() -> FinSequence, P1[ set , set , set ] } : ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) provided A1: for k being Element of NAT for x being set st 1 <= k & k < len F1() holds ex y being set st P1[F1() . (k + 1),x,y] proof defpred S1[ Element of NAT , set , set ] means P1[F1() . (\$1 + 1),\$2,\$3]; A2: for k being Element of NAT st 1 <= k & k < len F1() holds for x being set ex y being set st S1[k,x,y] by A1; consider p being FinSequence such that A3: ( len p = len F1() & ( p . 1 = F1() . 1 or len F1() = 0 ) & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[k,p . k,p . (k + 1)] ) ) from RECDEF_1:sch_3(A2); A4: ( len F1() <> 0 implies ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ) proof assume A5: len F1() <> 0 ; ::_thesis: ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) take p . (len p) ; ::_thesis: ex p being FinSequence st ( p . (len p) = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) take p ; ::_thesis: ( p . (len p) = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) thus ( p . (len p) = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) by A3, A5; ::_thesis: for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] let k be Element of NAT ; ::_thesis: ( 1 <= k & k < len F1() implies P1[F1() . (k + 1),p . k,p . (k + 1)] ) assume ( 1 <= k & k < len F1() ) ; ::_thesis: P1[F1() . (k + 1),p . k,p . (k + 1)] hence P1[F1() . (k + 1),p . k,p . (k + 1)] by A3; ::_thesis: verum end; ( len F1() = 0 implies ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ) proof assume A6: len F1() = 0 ; ::_thesis: ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) take F1() . 0 ; ::_thesis: ex p being FinSequence st ( F1() . 0 = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) take F1() ; ::_thesis: ( F1() . 0 = F1() . (len F1()) & len F1() = len F1() & F1() . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),F1() . k,F1() . (k + 1)] ) ) thus ( F1() . 0 = F1() . (len F1()) & len F1() = len F1() & F1() . 1 = F1() . 1 ) by A6; ::_thesis: for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),F1() . k,F1() . (k + 1)] thus for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),F1() . k,F1() . (k + 1)] by A6; ::_thesis: verum end; hence ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) by A4; ::_thesis: verum end; scheme :: RECDEF_1:sch 6 LambdaSeqBinOpEx{ F1() -> FinSequence, F2( set , set ) -> set } : ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) proof defpred S1[ set , set , set ] means \$3 = F2(\$1,\$2); A1: for k being Element of NAT for x being set st 1 <= k & k < len F1() holds ex y being set st S1[F1() . (k + 1),x,y] ; consider x being set such that A2: ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[F1() . (k + 1),p . k,p . (k + 1)] ) ) from RECDEF_1:sch_5(A1); take x ; ::_thesis: ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) consider p being FinSequence such that A3: ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) and A4: for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) by A2; take p ; ::_thesis: ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) thus ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) by A3; ::_thesis: for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) let k be Element of NAT ; ::_thesis: ( 1 <= k & k < len F1() implies p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) assume ( 1 <= k & k < len F1() ) ; ::_thesis: p . (k + 1) = F2((F1() . (k + 1)),(p . k)) hence p . (k + 1) = F2((F1() . (k + 1)),(p . k)) by A4; ::_thesis: verum end; scheme :: RECDEF_1:sch 7 FinRecUn{ F1() -> set , F2() -> Nat, F3() -> FinSequence, F4() -> FinSequence, P1[ set , set , set ] } : F3() = F4() provided A1: for n being Element of NAT st 1 <= n & n < F2() holds for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 and A2: ( len F3() = F2() & ( F3() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,F3() . n,F3() . (n + 1)] ) ) and A3: ( len F4() = F2() & ( F4() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,F4() . n,F4() . (n + 1)] ) ) proof defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= F2() & F3() . \$1 <> F4() . \$1 ); assume A4: F3() <> F4() ; ::_thesis: contradiction dom F3() = Seg (len F4()) by A2, A3, FINSEQ_1:def_3 .= dom F4() by FINSEQ_1:def_3 ; then consider x being set such that A5: x in dom F3() and A6: F3() . x <> F4() . x by A4, FUNCT_1:2; A7: x in Seg (len F3()) by A5, FINSEQ_1:def_3; reconsider x = x as Element of NAT by A5; A8: 1 <= x by A7, FINSEQ_1:1; x <= F2() by A2, A7, FINSEQ_1:1; then A9: ex n being Nat st S1[n] by A6, A8; consider n being Nat such that A10: ( S1[n] & ( for k being Nat st S1[k] holds n <= k ) ) from NAT_1:sch_5(A9); 0 <> n by A10; then consider k being Nat such that A11: n = k + 1 by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; n <> 1 by A2, A3, A10; then 1 < n by A10, XXREAL_0:1; then A12: 1 <= k by A11, NAT_1:13; k < n by A11, XREAL_1:29; then A13: k < F2() by A10, XXREAL_0:2; n > k by A11, NAT_1:13; then F3() . k = F4() . k by A10, A12, A13; then A14: P1[k,F3() . k,F4() . (k + 1)] by A3, A12, A13; P1[k,F3() . k,F3() . (k + 1)] by A2, A12, A13; hence contradiction by A1, A10, A11, A12, A13, A14; ::_thesis: verum end; scheme :: RECDEF_1:sch 8 FinRecUnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, F4() -> FinSequence of F1(), F5() -> FinSequence of F1(), P1[ set , set , set ] } : F4() = F5() provided A1: for n being Element of NAT st 1 <= n & n < F3() holds for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 and A2: ( len F4() = F3() & ( F4() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,F4() . n,F4() . (n + 1)] ) ) and A3: ( len F5() = F3() & ( F5() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,F5() . n,F5() . (n + 1)] ) ) proof defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= F3() & F4() . \$1 <> F5() . \$1 ); assume A4: F4() <> F5() ; ::_thesis: contradiction dom F4() = Seg (len F5()) by A2, A3, FINSEQ_1:def_3 .= dom F5() by FINSEQ_1:def_3 ; then consider x being set such that A5: x in dom F4() and A6: F4() . x <> F5() . x by A4, FUNCT_1:2; A7: x in Seg (len F4()) by A5, FINSEQ_1:def_3; reconsider x = x as Element of NAT by A5; A8: 1 <= x by A7, FINSEQ_1:1; x <= F3() by A2, A7, FINSEQ_1:1; then A9: ex n being Nat st S1[n] by A6, A8; consider n being Nat such that A10: ( S1[n] & ( for k being Nat st S1[k] holds n <= k ) ) from NAT_1:sch_5(A9); 0 <> n by A10; then consider k being Nat such that A11: n = k + 1 by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; reconsider Gk1 = F5() . (k + 1) as Element of F1() by A3, A10, A11, Lm1; n <> 1 by A2, A3, A10; then 1 < n by A10, XXREAL_0:1; then A12: 1 <= k by A11, NAT_1:13; k < n by A11, XREAL_1:29; then A13: k < F3() by A10, XXREAL_0:2; then reconsider Fk = F4() . k as Element of F1() by A2, A12, Lm1; n > k by A11, NAT_1:13; then F4() . k = F5() . k by A10, A12, A13; then A14: P1[k,Fk,Gk1] by A3, A12, A13; reconsider Fk1 = F4() . (k + 1) as Element of F1() by A2, A10, A11, Lm1; P1[k,Fk,Fk1] by A2, A12, A13; hence contradiction by A1, A10, A11, A12, A13, A14; ::_thesis: verum end; scheme :: RECDEF_1:sch 9 SeqBinOpUn{ F1() -> FinSequence, P1[ set , set , set ], F2() -> set , F3() -> set } : F2() = F3() provided A1: for k being Element of NAT for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds y1 = y2 and A2: ex p being FinSequence st ( F2() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) and A3: ex p being FinSequence st ( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) proof defpred S1[ Element of NAT , set , set ] means P1[F1() . (\$1 + 1),\$2,\$3]; A4: for k being Element of NAT st 1 <= k & k < len F1() holds for x, y1, y2 being set st S1[k,x,y1] & S1[k,x,y2] holds y1 = y2 by A1; consider q being FinSequence such that A5: F3() = q . (len q) and A6: ( len q = len F1() & q . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[k,q . k,q . (k + 1)] ) ) by A3; A7: ( len q = len F1() & ( q . 1 = F1() . 1 or len F1() = 0 ) & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[k,q . k,q . (k + 1)] ) ) by A6; consider p being FinSequence such that A8: F2() = p . (len p) and A9: ( len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[k,p . k,p . (k + 1)] ) ) by A2; A10: ( len p = len F1() & ( p . 1 = F1() . 1 or len F1() = 0 ) & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[k,p . k,p . (k + 1)] ) ) by A9; p = q from RECDEF_1:sch_7(A4, A10, A7); hence F2() = F3() by A8, A5; ::_thesis: verum end; scheme :: RECDEF_1:sch 10 LambdaSeqBinOpUn{ F1() -> FinSequence, F2( set , set ) -> set , F3() -> set , F4() -> set } : F3() = F4() provided A1: ex p being FinSequence st ( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) and A2: ex p being FinSequence st ( F4() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) proof defpred S1[ set , set , set ] means \$3 = F2(\$1,\$2); A3: ex p being FinSequence st ( F4() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[F1() . (k + 1),p . k,p . (k + 1)] ) ) by A2; A4: for k being Element of NAT for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & S1[z,x,y1] & S1[z,x,y2] holds y1 = y2 ; A5: ex p being FinSequence st ( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds S1[F1() . (k + 1),p . k,p . (k + 1)] ) ) by A1; thus F3() = F4() from RECDEF_1:sch_9(A4, A5, A3); ::_thesis: verum end; scheme :: RECDEF_1:sch 11 DefRec{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } : ( ex y being set ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 ) ) provided A1: for n being Element of NAT for x being set ex y being set st P1[n,x,y] and A2: for n being Element of NAT for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 proof A3: for n being Element of NAT for x being set ex y being set st P1[n,x,y] by A1; consider f being Function such that A4: ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_1(A3); A5: for n being Nat for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 proof let n be Nat; ::_thesis: for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 n in NAT by ORDINAL1:def_12; hence for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 by A2; ::_thesis: verum end; thus ex y being set ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) ::_thesis: for y1, y2 being set st ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 proof take f . F2() ; ::_thesis: ex f being Function st ( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) take f ; ::_thesis: ( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) thus ( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) by A4; ::_thesis: verum end; let y1, y2 be set ; ::_thesis: ( ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) implies y1 = y2 ) given f1 being Function such that A6: y1 = f1 . F2() and A7: dom f1 = NAT and A8: f1 . 0 = F1() and A9: for n being Element of NAT holds P1[n,f1 . n,f1 . (n + 1)] ; ::_thesis: ( for f being Function holds ( not y2 = f . F2() or not dom f = NAT or not f . 0 = F1() or ex n being Element of NAT st P1[n,f . n,f . (n + 1)] ) or y1 = y2 ) A10: for n being Nat holds P1[n,f1 . n,f1 . (n + 1)] proof let n be Nat; ::_thesis: P1[n,f1 . n,f1 . (n + 1)] n in NAT by ORDINAL1:def_12; hence P1[n,f1 . n,f1 . (n + 1)] by A9; ::_thesis: verum end; given f2 being Function such that A11: y2 = f2 . F2() and A12: dom f2 = NAT and A13: f2 . 0 = F1() and A14: for n being Element of NAT holds P1[n,f2 . n,f2 . (n + 1)] ; ::_thesis: y1 = y2 A15: for n being Nat holds P1[n,f2 . n,f2 . (n + 1)] proof let n be Nat; ::_thesis: P1[n,f2 . n,f2 . (n + 1)] n in NAT by ORDINAL1:def_12; hence P1[n,f2 . n,f2 . (n + 1)] by A14; ::_thesis: verum end; f1 = f2 from NAT_1:sch_13(A7, A8, A10, A12, A13, A15, A5); hence y1 = y2 by A6, A11; ::_thesis: verum end; scheme :: RECDEF_1:sch 12 LambdaDefRec{ F1() -> set , F2() -> Nat, F3( set , set ) -> set } : ( ex y being set ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ( for y1, y2 being set st ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) holds y1 = y2 ) ) proof defpred S1[ set , set , set ] means for z being set st z = \$2 holds \$3 = F3(\$1,z); A1: for n being Element of NAT for x being set ex y being set st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y] let x be set ; ::_thesis: ex y being set st S1[n,x,y] take F3(n,x) ; ::_thesis: S1[n,x,F3(n,x)] let z be set ; ::_thesis: ( z = x implies F3(n,x) = F3(n,z) ) assume z = x ; ::_thesis: F3(n,x) = F3(n,z) hence F3(n,x) = F3(n,z) ; ::_thesis: verum end; A2: for n being Element of NAT for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds y1 = y2 proof let n be Element of NAT ; ::_thesis: for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds y1 = y2 let x, y1, y2 be set ; ::_thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 ) assume that A3: for z being set st z = x holds y1 = F3(n,z) and A4: for z being set st z = x holds y2 = F3(n,z) ; ::_thesis: y1 = y2 thus y1 = F3(n,x) by A3 .= y2 by A4 ; ::_thesis: verum end; A5: ( ex y being set ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 ) ) from RECDEF_1:sch_11(A1, A2); then consider y being set , f being Function such that A6: ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) ; thus ex y being set ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) ::_thesis: for y1, y2 being set st ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) holds y1 = y2 proof take y ; ::_thesis: ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) take f ; ::_thesis: ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) thus ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) by A6; ::_thesis: verum end; let y1, y2 be set ; ::_thesis: ( ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) implies y1 = y2 ) given f1 being Function such that A7: ( y1 = f1 . F2() & dom f1 = NAT & f1 . 0 = F1() ) and A8: for n being Element of NAT holds f1 . (n + 1) = F3(n,(f1 . n)) ; ::_thesis: ( for f being Function holds ( not y2 = f . F2() or not dom f = NAT or not f . 0 = F1() or ex n being Element of NAT st not f . (n + 1) = F3(n,(f . n)) ) or y1 = y2 ) A9: for n being Element of NAT holds S1[n,f1 . n,f1 . (n + 1)] by A8; given f2 being Function such that A10: ( y2 = f2 . F2() & dom f2 = NAT & f2 . 0 = F1() ) and A11: for n being Element of NAT holds f2 . (n + 1) = F3(n,(f2 . n)) ; ::_thesis: y1 = y2 for n being Element of NAT holds S1[n,f2 . n,f2 . (n + 1)] by A11; hence y1 = y2 by A5, A7, A10, A9; ::_thesis: verum end; scheme :: RECDEF_1:sch 13 DefRecD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } : ( ex y being Element of F1() ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 ) ) provided A1: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st P1[n,x,y] and A2: for n being Element of NAT for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 proof A3: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st P1[n,x,y] by A1; consider f being Function of NAT,F1() such that A4: ( f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A3); A5: for n being Nat for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 proof let n be Nat; ::_thesis: for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 n in NAT by ORDINAL1:def_12; hence for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 by A2; ::_thesis: verum end; thus ex y being Element of F1() ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) ::_thesis: for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 proof reconsider n = F3() as Element of NAT by ORDINAL1:def_12; take f . n ; ::_thesis: ex f being Function of NAT,F1() st ( f . n = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) take f ; ::_thesis: ( f . n = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) thus ( f . n = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) by A4; ::_thesis: verum end; let y1, y2 be Element of F1(); ::_thesis: ( ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) implies y1 = y2 ) given f1 being Function of NAT,F1() such that A6: y1 = f1 . F3() and A7: f1 . 0 = F2() and A8: for n being Element of NAT holds P1[n,f1 . n,f1 . (n + 1)] ; ::_thesis: ( for f being Function of NAT,F1() holds ( not y2 = f . F3() or not f . 0 = F2() or ex n being Element of NAT st P1[n,f . n,f . (n + 1)] ) or y1 = y2 ) A9: f1 . 0 = F2() by A7; A10: for n being Nat holds P1[n,f1 . n,f1 . (n + 1)] proof let n be Nat; ::_thesis: P1[n,f1 . n,f1 . (n + 1)] n in NAT by ORDINAL1:def_12; hence P1[n,f1 . n,f1 . (n + 1)] by A8; ::_thesis: verum end; given f2 being Function of NAT,F1() such that A11: y2 = f2 . F3() and A12: f2 . 0 = F2() and A13: for n being Element of NAT holds P1[n,f2 . n,f2 . (n + 1)] ; ::_thesis: y1 = y2 A14: for n being Nat holds P1[n,f2 . n,f2 . (n + 1)] proof let n be Nat; ::_thesis: P1[n,f2 . n,f2 . (n + 1)] n in NAT by ORDINAL1:def_12; hence P1[n,f2 . n,f2 . (n + 1)] by A13; ::_thesis: verum end; A15: f2 . 0 = F2() by A12; f1 = f2 from NAT_1:sch_14(A9, A10, A15, A14, A5); hence y1 = y2 by A6, A11; ::_thesis: verum end; scheme :: RECDEF_1:sch 14 LambdaDefRecD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, F4( set , set ) -> Element of F1() } : ( ex y being Element of F1() ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds y1 = y2 ) ) proof defpred S1[ set , set , set ] means for z being Element of F1() st z = \$2 holds \$3 = F4(\$1,z); A1: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y] let x be Element of F1(); ::_thesis: ex y being Element of F1() st S1[n,x,y] take F4(n,x) ; ::_thesis: S1[n,x,F4(n,x)] let z be Element of F1(); ::_thesis: ( z = x implies F4(n,x) = F4(n,z) ) assume z = x ; ::_thesis: F4(n,x) = F4(n,z) hence F4(n,x) = F4(n,z) ; ::_thesis: verum end; A2: for n being Element of NAT for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds y1 = y2 proof let n be Element of NAT ; ::_thesis: for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds y1 = y2 let x, y1, y2 be Element of F1(); ::_thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 ) assume that A3: for z being Element of F1() st z = x holds y1 = F4(n,z) and A4: for z being Element of F1() st z = x holds y2 = F4(n,z) ; ::_thesis: y1 = y2 thus y1 = F4(n,x) by A3 .= y2 by A4 ; ::_thesis: verum end; A5: ( ex y being Element of F1() ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 ) ) from RECDEF_1:sch_13(A1, A2); then consider y being Element of F1(), f being Function of NAT,F1() such that A6: ( y = f . F3() & f . 0 = F2() ) and A7: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ; thus ex y being Element of F1() ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) ::_thesis: for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds y1 = y2 proof take y ; ::_thesis: ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) take f ; ::_thesis: ( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) thus ( y = f . F3() & f . 0 = F2() ) by A6; ::_thesis: for n being Nat holds f . (n + 1) = F4(n,(f . n)) let n be Nat; ::_thesis: f . (n + 1) = F4(n,(f . n)) reconsider n = n as Element of NAT by ORDINAL1:def_12; S1[n,f . n,f . (n + 1)] by A7; hence f . (n + 1) = F4(n,(f . n)) ; ::_thesis: verum end; let y1, y2 be Element of F1(); ::_thesis: ( ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) implies y1 = y2 ) given f being Function of NAT,F1() such that A8: ( y1 = f . F3() & f . 0 = F2() ) and A9: for n being Nat holds f . (n + 1) = F4(n,(f . n)) ; ::_thesis: ( for f being Function of NAT,F1() holds ( not y2 = f . F3() or not f . 0 = F2() or ex n being Nat st not f . (n + 1) = F4(n,(f . n)) ) or y1 = y2 ) A10: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] by A9; given f2 being Function of NAT,F1() such that A11: ( y2 = f2 . F3() & f2 . 0 = F2() ) and A12: for n being Nat holds f2 . (n + 1) = F4(n,(f2 . n)) ; ::_thesis: y1 = y2 for n being Element of NAT holds S1[n,f2 . n,f2 . (n + 1)] by A12; hence y1 = y2 by A5, A8, A11, A10; ::_thesis: verum end; scheme :: RECDEF_1:sch 15 SeqBinOpDef{ F1() -> FinSequence, P1[ set , set , set ] } : ( ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ( for x, y being set st ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) holds x = y ) ) provided A1: for k being Element of NAT for y being set st 1 <= k & k < len F1() holds ex z being set st P1[F1() . (k + 1),y,z] and A2: for k being Element of NAT for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds y1 = y2 proof A3: for k being Element of NAT for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds y1 = y2 by A2; A4: for k being Element of NAT for y being set st 1 <= k & k < len F1() holds ex z being set st P1[F1() . (k + 1),y,z] by A1; thus ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) from RECDEF_1:sch_5(A4); ::_thesis: for x, y being set st ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) holds x = y let x, y be set ; ::_thesis: ( ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) implies x = y ) assume A5: ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ; ::_thesis: ( for p being FinSequence holds ( not y = p . (len p) or not len p = len F1() or not p . 1 = F1() . 1 or ex k being Element of NAT st ( 1 <= k & k < len F1() & P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) or x = y ) assume A6: ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ; ::_thesis: x = y thus x = y from RECDEF_1:sch_9(A3, A5, A6); ::_thesis: verum end; scheme :: RECDEF_1:sch 16 LambdaSeqBinOpDef{ F1() -> FinSequence, F2( set , set ) -> set } : ( ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ( for x, y being set st ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) holds x = y ) ) proof thus ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) from RECDEF_1:sch_6(); ::_thesis: for x, y being set st ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) holds x = y let x, y be set ; ::_thesis: ( ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) implies x = y ) assume A1: ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) ; ::_thesis: ( for p being FinSequence holds ( not y = p . (len p) or not len p = len F1() or not p . 1 = F1() . 1 or ex k being Element of NAT st ( 1 <= k & k < len F1() & not p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) or x = y ) assume A2: ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) ; ::_thesis: x = y thus x = y from RECDEF_1:sch_10(A1, A2); ::_thesis: verum end; scheme :: RECDEF_1:sch 17 SeqExD{ F1() -> non empty set , F2() -> Element of NAT , P1[ set , set ] } : ex p being FinSequence of F1() st ( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,p /. k] ) ) provided A1: for k being Element of NAT st k in Seg F2() holds ex x being Element of F1() st P1[k,x] proof percases ( F2() = 0 or F2() <> 0 ) ; supposeA2: F2() = 0 ; ::_thesis: ex p being FinSequence of F1() st ( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,p /. k] ) ) take <*> F1() ; ::_thesis: ( dom (<*> F1()) = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,(<*> F1()) /. k] ) ) thus ( dom (<*> F1()) = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,(<*> F1()) /. k] ) ) by A2; ::_thesis: verum end; supposeA3: F2() <> 0 ; ::_thesis: ex p being FinSequence of F1() st ( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,p /. k] ) ) now__::_thesis:_not_Seg_F2()_=_{} assume A4: Seg F2() = {} ; ::_thesis: contradiction now__::_thesis:_(_(_F2()_=_0_&_contradiction_)_or_(_F2()_<>_0_&_contradiction_)_) percases ( F2() = 0 or F2() <> 0 ) ; case F2() = 0 ; ::_thesis: contradiction hence contradiction by A3; ::_thesis: verum end; case F2() <> 0 ; ::_thesis: contradiction hence contradiction by A4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; then reconsider M = Seg F2() as non empty set ; A5: for x being Element of M ex y being Element of F1() st P1[x,y] proof let x be Element of M; ::_thesis: ex y being Element of F1() st P1[x,y] x in Seg F2() ; hence ex y being Element of F1() st P1[x,y] by A1; ::_thesis: verum end; consider f being Function of M,F1() such that A6: for x being Element of M holds P1[x,f . x] from FUNCT_2:sch_3(A5); dom f = Seg F2() by FUNCT_2:def_1; then reconsider q = f as FinSequence by FINSEQ_1:def_2; now__::_thesis:_for_u_being_set_st_u_in_rng_q_holds_ u_in_F1() let u be set ; ::_thesis: ( u in rng q implies u in F1() ) A7: rng q c= F1() by RELAT_1:def_19; assume u in rng q ; ::_thesis: u in F1() hence u in F1() by A7; ::_thesis: verum end; then rng q c= F1() by TARSKI:def_3; then reconsider q = q as FinSequence of F1() by FINSEQ_1:def_4; take q ; ::_thesis: ( dom q = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,q /. k] ) ) now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_Seg_F2()_holds_ P1[k,q_/._k] let k be Element of NAT ; ::_thesis: ( k in Seg F2() implies P1[k,q /. k] ) assume A8: k in Seg F2() ; ::_thesis: P1[k,q /. k] then k in dom q by FUNCT_2:def_1; then q . k = q /. k by PARTFUN1:def_6; hence P1[k,q /. k] by A6, A8; ::_thesis: verum end; hence ( dom q = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,q /. k] ) ) by FUNCT_2:def_1; ::_thesis: verum end; end; end; scheme :: RECDEF_1:sch 18 FinRecExD2{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of NAT , P1[ set , set , set ] } : ex p being FinSequence of F1() st ( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds P1[n,p /. n,p /. (n + 1)] ) ) provided A1: for n being Element of NAT st 1 <= n & n <= F3() - 1 holds for x being Element of F1() ex y being Element of F1() st P1[n,x,y] proof set 00 = the Element of F1(); defpred S1[ Element of NAT , set , set ] means ( ( 0 <= \$1 & \$1 <= F3() - 2 implies P1[\$1 + 1,\$2,\$3] ) & ( ( not 0 <= \$1 or not \$1 <= F3() - 2 ) implies \$3 = the Element of F1() ) ); A2: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y] let x be Element of F1(); ::_thesis: ex y being Element of F1() st S1[n,x,y] ( 0 <= n & n <= F3() - 2 implies ex y being Element of F1() st S1[n,x,y] ) proof A3: 0 + 1 <= n + 1 by XREAL_1:6; assume that 0 <= n and A4: n <= F3() - 2 ; ::_thesis: ex y being Element of F1() st S1[n,x,y] n + 1 <= (F3() - 2) + 1 by A4, XREAL_1:6; then consider y being Element of F1() such that A5: P1[n + 1,x,y] by A1, A3; take y ; ::_thesis: S1[n,x,y] thus ( 0 <= n & n <= F3() - 2 implies P1[n + 1,x,y] ) by A5; ::_thesis: ( ( not 0 <= n or not n <= F3() - 2 ) implies y = the Element of F1() ) thus ( ( not 0 <= n or not n <= F3() - 2 ) implies y = the Element of F1() ) by A4; ::_thesis: verum end; hence ex y being Element of F1() st S1[n,x,y] ; ::_thesis: verum end; consider f being Function of NAT,F1() such that A6: ( f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A2); defpred S2[ set , set ] means for r being Real st r = \$1 holds \$2 = f . (r - 1); A7: for x being set st x in REAL holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in REAL implies ex y being set st S2[x,y] ) assume x in REAL ; ::_thesis: ex y being set st S2[x,y] then reconsider r = x as Real ; take f . (r - 1) ; ::_thesis: S2[x,f . (r - 1)] thus S2[x,f . (r - 1)] ; ::_thesis: verum end; consider g being Function such that A8: ( dom g = REAL & ( for x being set st x in REAL holds S2[x,g . x] ) ) from CLASSES1:sch_1(A7); A9: dom (g | (Seg F3())) = Seg F3() by A8, RELAT_1:62, XBOOLE_1:1; then reconsider p = g | (Seg F3()) as FinSequence by FINSEQ_1:def_2; now__::_thesis:_for_x_being_set_st_x_in_rng_p_holds_ x_in_F1() let x be set ; ::_thesis: ( x in rng p implies x in F1() ) assume x in rng p ; ::_thesis: x in F1() then consider y being set such that A10: y in dom p and A11: x = p . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A10; A12: f . (y - 1) in F1() proof y <> 0 by A9, A10, FINSEQ_1:1; then consider k being Nat such that A13: y = k + 1 by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; f . k in F1() ; hence f . (y - 1) in F1() by A13; ::_thesis: verum end; p . y = g . y by A10, FUNCT_1:47; hence x in F1() by A8, A11, A12; ::_thesis: verum end; then rng p c= F1() by TARSKI:def_3; then reconsider p = p as FinSequence of F1() by FINSEQ_1:def_4; take p ; ::_thesis: ( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds P1[n,p /. n,p /. (n + 1)] ) ) thus len p = F3() by A9, FINSEQ_1:def_3; ::_thesis: ( ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds P1[n,p /. n,p /. (n + 1)] ) ) ( F3() <> 0 implies p /. 1 = F2() ) proof assume F3() <> 0 ; ::_thesis: p /. 1 = F2() then consider k being Nat such that A14: F3() = k + 1 by NAT_1:6; 0 + 1 <= k + 1 by XREAL_1:7; then A15: 1 in Seg F3() by A14, FINSEQ_1:1; then p /. 1 = p . 1 by A9, PARTFUN1:def_6 .= g . 1 by A15, FUNCT_1:49 .= f . (1 - 1) by A8 .= F2() by A6 ; hence p /. 1 = F2() ; ::_thesis: verum end; hence ( p /. 1 = F2() or F3() = 0 ) ; ::_thesis: for n being Element of NAT st 1 <= n & n <= F3() - 1 holds P1[n,p /. n,p /. (n + 1)] let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= F3() - 1 implies P1[n,p /. n,p /. (n + 1)] ) assume that A16: 1 <= n and A17: n <= F3() - 1 ; ::_thesis: P1[n,p /. n,p /. (n + 1)] consider k being Nat such that A18: n = k + 1 by A16, NAT_1:6; A19: for n being Element of NAT st n <= F3() - 1 holds p /. (n + 1) = f . n proof let n be Element of NAT ; ::_thesis: ( n <= F3() - 1 implies p /. (n + 1) = f . n ) assume n <= F3() - 1 ; ::_thesis: p /. (n + 1) = f . n then A20: n + 1 <= (F3() - 1) + 1 by XREAL_1:6; A21: g . (n + 1) = f . ((n + 1) - 1) by A8 .= f . n ; 1 <= n + 1 by NAT_1:11; then A22: n + 1 in Seg F3() by A20, FINSEQ_1:1; then p /. (n + 1) = p . (n + 1) by A9, PARTFUN1:def_6; hence p /. (n + 1) = f . n by A22, A21, FUNCT_1:49; ::_thesis: verum end; A23: k <= k + 1 by NAT_1:11; A24: k in NAT by ORDINAL1:def_12; k <= (F3() - 1) - 1 by A17, A18, XREAL_1:19; then P1[k + 1,f . k,f . (k + 1)] by A6, A24; then P1[k + 1,f . k,p /. ((k + 1) + 1)] by A19, A17, A18; hence P1[n,p /. n,p /. (n + 1)] by A19, A17, A18, A24, A23, XXREAL_0:2; ::_thesis: verum end;