let p, q be AlgSequence of R; :: thesis: ( len p <= 1 & p . 0 = x & len q <= 1 & q . 0 = x implies p = q )
assume that
A2: ( len p <= 1 & p . 0 = x ) and
A3: ( len q <= 1 & q . 0 = x ) ; :: thesis: p = q
A4: 1 = 0 + 1 ;

A5: now

assume x = 0. R ; :: thesis: len p = len q
then ( len p <> 1 & len q <> 1 ) by A2, A3, A4, Th25;
then ( len p < 1 & len q < 1 ) by A2, A3, XXREAL_0:1;
then ( len p = 0 & len q = 0 ) by NAT_1:14;
hence len p = len q ; :: thesis: verum

end;

A6: now

assume x <> 0. R ; :: thesis: len p = len q
then ( len p = 1 & len q = 1 ) by A2, A3, A4, Th22, NAT_1:8;
hence len p = len q ; :: thesis: verum

end;

for k being Nat st k < len p holds
p . k = q . k

proof

let k be Nat; :: thesis: ( k < len p implies p . k = q . k )
assume k < len p ; :: thesis: p . k = q . k
then k < 1 by A2, XXREAL_0:2;
then k = 0 by NAT_1:14;
hence p . k = q . k by A2, A3; :: thesis: verum

end;

hence p = q by A5, A6, Th28; :: thesis: verum