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 S1[ 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 \ {()}),(y \ {()})] in \$2 ) } ;
A1: for n being Nat
for x being set ex y being set st S1[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 & [(),()] in the InternalRel of R ) ) } and
A4: for n being Nat holds S1[n,f . n,f . (n + 1)] from A5: for n being Nat holds S1[n,f . n,f . (n + 1)] by A4;
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):] ) )
thus dom f = NAT by A2; :: thesis: for x being object st x in NAT holds
f . b2 in bool [:(Fin the carrier of R),(Fin the carrier of R):]

let x be object ; :: thesis: ( x in NAT implies f . b1 in bool [:(Fin the carrier of R),(Fin the carrier of R):] )
assume x in NAT ; :: thesis: f . b1 in bool [:(Fin the carrier of R),(Fin the carrier of R):]
then reconsider x9 = x as Element of NAT ;
per cases ( x9 = 0 or x9 > 0 ) ;
suppose A6: x9 = 0 ; :: thesis: f . b1 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 & [(),()] in the InternalRel of R ) ) } ;
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 & [(),()] in the InternalRel of R ) ) } holds
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 & [(),()] 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 & [(),()] 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 & [(),()] in the InternalRel of R ) ) ) ;
hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: thesis: verum
end;
then { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(),()] in the InternalRel of R ) ) } c= [:(Fin the carrier of R),(Fin the carrier of R):] ;
hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A3, A6; :: thesis: verum
end;
suppose A7: x9 > 0 ; :: thesis: f . b1 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 ;
set FX = { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {()}),(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 \ {()}),(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 \ {()}),(b \ {()})] in f . x1 ) } holds
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 \ {()}),(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 \ {()}),(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 \ {()}),(b \ {()})] in f . x1 ) ;
hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: thesis: verum
end;
then { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {()}),(b \ {()})] in f . x1 ) } c= [:(Fin the carrier of R),(Fin the carrier of R):] ;
hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A9; :: thesis: verum
end;
end;
end;
then reconsider f = f as sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) by FUNCT_2:3;
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 & [(),()] 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 \ {()}),(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 & [(),()] 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 \ {()}),(y \ {()})] in f . n ) } ) ) by A2, A3, A5; :: thesis: verum