let IT1, IT2 be sequence of (bool NAT); :: thesis: ( IT1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Nat
for sn being non empty Subset of NAT st IT1 . i = sn holds
IT1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds IT1 . i is infinite ) & IT2 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Nat
for sn being non empty Subset of NAT st IT2 . i = sn holds
IT2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds IT2 . i is infinite ) implies IT1 = IT2 )
assume that
A19: IT1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } and
A20: for i being Nat
for sn being non empty Subset of NAT st IT1 . i = sn holds
IT1 . (i + 1) = sn \ {(min sn)} and
for i being Nat holds IT1 . i is infinite and
A21: IT2 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } and
A22: for i being Nat
for sn being non empty Subset of NAT st IT2 . i = sn holds
IT2 . (i + 1) = sn \ {(min sn)} and
A23: for i being Nat holds IT2 . i is infinite ; :: thesis: IT1 = IT2

now :: thesis: ( NAT = dom IT1 & NAT = dom IT2 & ( for x being object st x in NAT holds
IT1 . x = IT2 . x ) )

defpred S₁[ Nat] means IT1 . $1 = IT2 . $1;
thus NAT = dom IT1 by FUNCT_2:def 1; :: thesis: ( NAT = dom IT2 & ( for x being object st x in NAT holds
IT1 . x = IT2 . x ) )
thus NAT = dom IT2 by FUNCT_2:def 1; :: thesis: for x being object st x in NAT holds
IT1 . x = IT2 . x
A24: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A25: IT1 . n = IT2 . n ; :: thesis: S₁[n + 1]
then reconsider IT1n = IT1 . n as non empty Subset of NAT by A23;
thus IT1 . (n + 1) = IT1n \ {(min IT1n)} by A20
.= IT2 . (n + 1) by A22, A25 ; :: thesis: verum

end;

A26: S₁[ 0 ] by A19, A21;
for n being Nat holds S₁[n] from NAT_1:sch 2(A26, A24);
hence for x being object st x in NAT holds
IT1 . x = IT2 . x ; :: thesis: verum

end;

hence IT1 = IT2 ; :: thesis: verum