let f be FinSequence of the Instructions of SCM+FSA ; :: thesis: card (Load f) = len f

A1: now

let i, j be Element of NAT ; :: thesis: ( i in dom f & j in dom f & H₁(i) = H₁(j) implies i = j )
assume that
A2: ( i in dom f & j in dom f ) and
A3: H₁(i) = H₁(j) ; :: thesis: i = j
ex n being Nat st dom f = Seg n by FINSEQ_1:def 2;
then ( 1 <= i & 1 <= j ) by A2, FINSEQ_1:3;
hence i = j by A3, XREAL_1:236; :: thesis: verum

end;

set X = { H₁(m) where m is Element of NAT : m in dom f } ;
A4: dom f c= NAT ;
A5: dom f,{ H₁(m) where m is Element of NAT : m in dom f } are_equipotent from FUNCT_7:sch 6(A4, A1);
A6: dom f is finite ;
{ H₁(m) where m is Element of NAT : m in dom f } is finite from FRAENKEL:sch 21(A6);
then reconsider X = { H₁(m) where m is Element of NAT : m in dom f } as finite set ;
A7: dom (Load f) = X by Def1;
reconsider T = dom f as finite set ;
A8: T = Seg (len f) by FINSEQ_1:def 3;
thus card (Load f) = card (dom (Load f)) by CARD_1:104
.= card T by A5, A7, CARD_1:21
.= len (Sgm (Seg (len f))) by A8, FINSEQ_3:44
.= len f by FINSEQ_3:52 ; :: thesis: verum