let m be positive Nat; :: thesis: card (bool ((Seg m) \ {1})) = 2 |^ (m -' 1)
defpred S₁[ Nat] means card (bool ((Seg (1 + $1)) \ {1})) = 2 |^ $1;
(Seg (1 + 0)) \ {1} = {} by FINSEQ_1:2;
then card (bool ((Seg (1 + 0)) \ {1})) = 1 by ZFMISC_1:1, CARD_1:30;
then A1: S₁[ 0 ] by NEWTON:4;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then card (bool ((Seg (1 + (n + 1))) \ {1})) = 2 * (2 |^ n) by HILB10_7:9
.= 2 |^ (n + 1) by NEWTON:6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A3: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
reconsider m1 = m - 1 as Nat ;
card (bool ((Seg (1 + m1)) \ {1})) = 2 |^ m1 by A3;
hence card (bool ((Seg m) \ {1})) = 2 |^ (m -' 1) ; :: thesis: verum