let R be non empty ZeroStr ; :: thesis: for p, q being AlgSequence of R st len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) holds
p = q
let p, q be AlgSequence of R; :: thesis: ( len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) implies p = q )
assume A1: ( len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) ) ; :: thesis: p = q
A2: ( dom p = NAT & dom q = NAT ) by FUNCT_2:def 1;
for x being set st x in NAT holds
p . x = q . x

proof

let x be set ; :: thesis: ( x in NAT implies p . x = q . x )
assume x in NAT ; :: thesis: p . x = q . x
then reconsider k = x as Element of NAT ;
p . k = q . k

proof

( k >= len p implies p . k = q . k )

proof

assume k >= len p ; :: thesis: p . k = q . k
then ( p . k = 0. R & q . k = 0. R ) by A1, Th22;
hence p . k = q . k ; :: thesis: verum

end;

hence p . k = q . k by A1; :: thesis: verum

end;

hence p . x = q . x ; :: thesis: verum

end;

hence p = q by A2, FUNCT_1:9; :: thesis: verum