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 that

A1: len p = len q and

A2: for k being Nat st k < len p holds

p . k = q . k ; :: thesis: p = q

A3: for x being object st x in NAT holds

p . x = q . x

hence p = q by A3, FUNCT_1:2; :: thesis: verum

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 that

A1: len p = len q and

A2: for k being Nat st k < len p holds

p . k = q . k ; :: thesis: p = q

A3: for x being object st x in NAT holds

p . x = q . x

proof

( dom p = NAT & dom q = NAT )
by FUNCT_2:def 1;
let x be object ; :: 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 ;

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

end;assume x in NAT ; :: thesis: p . x = q . x

then reconsider k = x as Element of NAT ;

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

proof

hence
p . x = q . x
by A2; :: thesis: verum
assume A4:
k >= len p
; :: thesis: p . k = q . k

then p . k = 0. R by Th1;

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

end;then p . k = 0. R by Th1;

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

hence p = q by A3, FUNCT_1:2; :: thesis: verum