set IR = the InternalRel of R;
set CR = the carrier of R;
set FBCP = [:(Fin the carrier of R),(Fin the carrier of R):];
let IT1, IT2 be sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]); :: thesis: ( dom IT1 = NAT & IT1 . 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 IT1 . (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 IT1 . n ) } ) & dom IT2 = NAT & IT2 . 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 IT2 . (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 IT2 . n ) } ) implies IT1 = IT2 )
assume that
A10: dom IT1 = NAT and
A11: IT1 . 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
A12: for n being Nat holds IT1 . (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 IT1 . n ) } and
A13: dom IT2 = NAT and
A14: IT2 . 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
A15: for n being Nat holds IT2 . (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 IT2 . n ) } ; :: thesis: IT1 = IT2
defpred S₁[ 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 ) } ;
A16: dom IT1 = NAT by A10;
A17: IT1 . 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 ) ) } by A11;
A18: for n being Nat holds S₁[n,IT1 . n,IT1 . (n + 1)] by A12;
A19: dom IT2 = NAT by A13;
A20: IT2 . 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 ) ) } by A14;
A21: for n being Nat holds S₁[n,IT2 . n,IT2 . (n + 1)] by A15;
A22: for n being Nat
for x, y1, y2 being set st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
thus IT1 = IT2 from NAT_1:sch 13(A16, A17, A18, A19, A20, A21, A22); :: thesis: verum