let fa, fb be FinSequence of NAT ; :: thesis: ( len fa = len f & ( for i being Nat st i in dom f holds
fa . i = (f . i) mod m ) & len fb = len f & ( for i being Nat st i in dom f holds
fb . i = (f . i) mod m ) implies fa = fb )
assume that
A5: len f = len fa and
A6: for i being Nat st i in dom f holds
fa . i = (f . i) mod m and
A7: len f = len fb and
A8: for i being Nat st i in dom f holds
fb . i = (f . i) mod m ; :: thesis: fa = fb

now

let X be set ; :: thesis: ( dom f = X implies fa = fb )
assume A9: dom f = X ; :: thesis: fa = fb
A10: for i being Nat st i in X holds
fa . i = fb . i

proof

given j being Nat such that A11: j in X and
A12: fa . j <> fb . j ; :: thesis: contradiction
fa . j <> (f . j) mod m by A8, A9, A11, A12;
hence contradiction by A6, A9, A11; :: thesis: verum

end;

A13: dom f = Seg (len f) by FINSEQ_1:def 3
.= dom fb by A7, FINSEQ_1:def 3 ;
dom f = Seg (len f) by FINSEQ_1:def 3
.= dom fa by A5, FINSEQ_1:def 3 ;
hence fa = fb by A9, A13, A10, FINSEQ_1:13; :: thesis: verum

end;

hence fa = fb ; :: thesis: verum