let S be set ; :: thesis: for s being FinSequence of S holds card (whole_event ) = len s
let s be FinSequence of S; :: thesis: card (whole_event ) = len s
thus card (whole_event ) = card (Seg (len s)) by FINSEQ_1:def 3
.= len s by FINSEQ_1:57 ; :: thesis: verum