let R be domRing; :: thesis: for G being FinSequence of the carrier of R holds
( G = (len G) |-> (0. R) iff for i being Nat st i in dom G holds
G . i = 0. R )
let G be FinSequence of the carrier of R; :: thesis: ( G = (len G) |-> (0. R) iff for i being Nat st i in dom G holds
G . i = 0. R )
( ( for i being Nat st i in dom G holds
G . i = 0. R ) implies G = (len G) |-> (0. R) )

proof

assume A2: for i being Nat st i in dom G holds
G . i = 0. R ; :: thesis: G = (len G) |-> (0. R)
for k being Nat st 1 <= k & k <= len G holds
G . k = ((len G) |-> (0. R)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len G implies G . k = ((len G) |-> (0. R)) . k )
assume A4: ( 1 <= k & k <= len G ) ; :: thesis: G . k = ((len G) |-> (0. R)) . k
then A6: k in dom ((len G) |-> (0. R)) ;
G . k = 0. R by A2, A4, FINSEQ_3:25
.= ((len G) |-> (0. R)) . k by A6, FINSEQ_2:57 ;
hence G . k = ((len G) |-> (0. R)) . k ; :: thesis: verum

end;

hence G = (len G) |-> (0. R) ; :: thesis: verum

end;

hence ( G = (len G) |-> (0. R) iff for i being Nat st i in dom G holds
G . i = 0. R ) by FINSEQ_2:57; :: thesis: verum