let F be FinSequence of INT ; :: thesis: ( F = f mod m iff ( len F = len f & ( for i being object st i in dom f holds
F . i = (f . i) mod m ) ) )
thus ( F = f mod m implies ( len F = len f & ( for i being object st i in dom f holds
F . i = (f . i) mod m ) ) ) :: thesis: ( len F = len f & ( for i being object st i in dom f holds
F . i = (f . i) mod m ) implies F = f mod m )

proof

assume A1: F = f mod m ; :: thesis: ( len F = len f & ( for i being object st i in dom f holds
F . i = (f . i) mod m ) )
then dom F = dom f by Def1;
hence ( len F = len f & ( for i being object st i in dom f holds
F . i = (f . i) mod m ) ) by A1, Def1, FINSEQ_3:29; :: thesis: verum

end;

thus ( len F = len f & ( for i being object st i in dom f holds
F . i = (f . i) mod m ) implies F = f mod m ) by Def1, FINSEQ_3:29; :: thesis: verum