let S be non empty finite 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
card (whole_event ) = card (Seg (len s)) by FINSEQ_1:def 3
.= len s by FINSEQ_1:78 ;
hence card (whole_event ) = len s ; :: thesis: verum