set IR = the InternalRel of R;

set CR = the carrier of R;

set FBCP = [:(Fin the carrier of R),(Fin the carrier of R):];

defpred S_{1}[ Nat, set , set ] means $3 = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in $2 ) } ;

A1: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]
;

consider f being Function such that

A2: dom f = NAT and

A3: f . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } and

A4: for n being Nat holds S_{1}[n,f . n,f . (n + 1)]
from RECDEF_1:sch 1(A1);

A5: for n being Nat holds S_{1}[n,f . n,f . (n + 1)]
by A4;

take f ; :: thesis: ( dom f = NAT & f . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds f . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in f . n ) } ) )

thus ( dom f = NAT & f . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds f . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in f . n ) } ) ) by A2, A3, A5; :: thesis: verum

set CR = the carrier of R;

set FBCP = [:(Fin the carrier of R),(Fin the carrier of R):];

defpred S

A1: for n being Nat

for x being set ex y being set st S

consider f being Function such that

A2: dom f = NAT and

A3: f . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } and

A4: for n being Nat holds S

A5: for n being Nat holds S

now :: thesis: ( dom f = NAT & ( for x being object st x in NAT holds

f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] ) )

then reconsider f = f as sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) by FUNCT_2:3;f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] ) )

thus
dom f = NAT
by A2; :: thesis: for x being object st x in NAT holds

f . b_{2} in bool [:(Fin the carrier of R),(Fin the carrier of R):]

let x be object ; :: thesis: ( x in NAT implies f . b_{1} in bool [:(Fin the carrier of R),(Fin the carrier of R):] )

assume x in NAT ; :: thesis: f . b_{1} in bool [:(Fin the carrier of R),(Fin the carrier of R):]

then reconsider x9 = x as Element of NAT ;

end;f . b

let x be object ; :: thesis: ( x in NAT implies f . b

assume x in NAT ; :: thesis: f . b

then reconsider x9 = x as Element of NAT ;

per cases
( x9 = 0 or x9 > 0 )
;

end;

suppose A6:
x9 = 0
; :: thesis: f . b_{1} in bool [:(Fin the carrier of R),(Fin the carrier of R):]

set F0 = { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } ;

hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A3, A6; :: thesis: verum

end;now :: thesis: for z being object st z in { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } holds

z in [:(Fin the carrier of R),(Fin the carrier of R):]

then
{ [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } c= [:(Fin the carrier of R),(Fin the carrier of R):]
;z in [:(Fin the carrier of R),(Fin the carrier of R):]

let z be object ; :: thesis: ( z in { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } implies z in [:(Fin the carrier of R),(Fin the carrier of R):] )

assume z in { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } ; :: thesis: z in [:(Fin the carrier of R),(Fin the carrier of R):]

then ex a, b being Element of Fin the carrier of R st

( z = [a,b] & ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) ) ;

hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: thesis: verum

end;assume z in { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } ; :: thesis: z in [:(Fin the carrier of R),(Fin the carrier of R):]

then ex a, b being Element of Fin the carrier of R st

( z = [a,b] & ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) ) ;

hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: thesis: verum

hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A3, A6; :: thesis: verum

suppose A7:
x9 > 0
; :: thesis: f . b_{1} in bool [:(Fin the carrier of R),(Fin the carrier of R):]

A8:
x9 = (x9 - 1) + 1
;

reconsider x1 = x9 - 1 as Element of NAT by A7, NAT_1:20;

set FX = { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } ;

A9: { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } = f . x9 by A4, A8;

hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A9; :: thesis: verum

end;reconsider x1 = x9 - 1 as Element of NAT by A7, NAT_1:20;

set FX = { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } ;

A9: { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } = f . x9 by A4, A8;

now :: thesis: for z being object st z in { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } holds

z in [:(Fin the carrier of R),(Fin the carrier of R):]

then
{ [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } c= [:(Fin the carrier of R),(Fin the carrier of R):]
;z in [:(Fin the carrier of R),(Fin the carrier of R):]

let z be object ; :: thesis: ( z in { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } implies z in [:(Fin the carrier of R),(Fin the carrier of R):] )

assume z in { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } ; :: thesis: z in [:(Fin the carrier of R),(Fin the carrier of R):]

then ex a, b being Element of Fin the carrier of R st

( z = [a,b] & a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) ;

hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: thesis: verum

end;assume z in { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } ; :: thesis: z in [:(Fin the carrier of R),(Fin the carrier of R):]

then ex a, b being Element of Fin the carrier of R st

( z = [a,b] & a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) ;

hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: thesis: verum

hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A9; :: thesis: verum

take f ; :: thesis: ( dom f = NAT & f . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds f . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in f . n ) } ) )

thus ( dom f = NAT & f . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds f . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in f . n ) } ) ) by A2, A3, A5; :: thesis: verum