let k, m be Nat; :: thesis: card ((multiples 2) /\ (seq (k,(2 * m)))) = m
set M = multiples 2;
defpred S₁[ Nat] means card ((multiples 2) /\ (seq (k,(2 * $1)))) = $1;
A1: S₁[ 0 ]

proof

seq (k,(2 * 0)) = {} by CALCUL_2:2;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for z being Nat st S₁[z] holds
S₁[z + 1]

proof

let z be Nat; :: thesis: ( S₁[z] implies S₁[z + 1] )
assume A3: S₁[z] ; :: thesis: S₁[z + 1]
seq (k,(2 * (z + 1))) = seq (k,(((2 * z) + 1) + 1))
.= (seq (k,((2 * z) + 1))) \/ {((k + ((2 * z) + 1)) + 1)} by CALCUL_2:5
.= ((seq (k,(2 * z))) \/ {((k + (2 * z)) + 1)}) \/ {((k + ((2 * z) + 1)) + 1)} by CALCUL_2:5 ;
then A4: (multiples 2) /\ (seq (k,(2 * (z + 1)))) = (multiples 2) /\ ((seq (k,(2 * z))) \/ ({((k + (2 * z)) + 1)} \/ {((k + ((2 * z) + 1)) + 1)})) by XBOOLE_1:4
.= ((multiples 2) /\ (seq (k,(2 * z)))) \/ ((multiples 2) /\ ({((k + (2 * z)) + 1)} \/ {((k + ((2 * z) + 1)) + 1)})) by XBOOLE_1:23 ;
A5: {((k + (2 * z)) + 1)} \/ {((k + ((2 * z) + 1)) + 1)} = {((k + (2 * z)) + 1),((k + ((2 * z) + 1)) + 1)} by ENUMSET1:1;
seq (k,(2 * z)) misses {((k + (2 * z)) + 1),((k + (2 * z)) + 2)} by Th74;
then card (((multiples 2) /\ (seq (k,(2 * z)))) \/ ((multiples 2) /\ ({((k + (2 * z)) + 1)} \/ {((k + ((2 * z) + 1)) + 1)}))) = (card ((multiples 2) /\ (seq (k,(2 * z))))) + (card ((multiples 2) /\ ({((k + (2 * z)) + 1)} \/ {((k + ((2 * z) + 1)) + 1)}))) by A5, XBOOLE_1:76, CARD_2:40;
hence S₁[z + 1] by A3, A4, A5, Th82; :: thesis: verum

end;

for z being Nat holds S₁[z] from NAT_1:sch 2(A1, A2);
hence card ((multiples 2) /\ (seq (k,(2 * m)))) = m ; :: thesis: verum