{ i where i is Element of I : b1 . i <> b2 . i } c= I

card F = card F ;

hence card { i where i is Element of I : b1 . i <> b2 . i } is Nat ; :: thesis: verum

proof

then reconsider F = { i where i is Element of I : b1 . i <> b2 . i } as finite set by FINSET_1:1;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { i where i is Element of I : b1 . i <> b2 . i } or a in I )

assume a in { i where i is Element of I : b1 . i <> b2 . i } ; :: thesis: a in I

then ex i being Element of I st

( a = i & b1 . i <> b2 . i ) ;

hence a in I ; :: thesis: verum

end;assume a in { i where i is Element of I : b1 . i <> b2 . i } ; :: thesis: a in I

then ex i being Element of I st

( a = i & b1 . i <> b2 . i ) ;

hence a in I ; :: thesis: verum

card F = card F ;

hence card { i where i is Element of I : b1 . i <> b2 . i } is Nat ; :: thesis: verum