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 and
A3: p . 0 = x and
A4: len q <= 1 and
A5: q . 0 = x ; :: thesis: p = q
A6: 1 = 0 + 1 ;

A7: now :: thesis: ( x = 0. R implies len p = len q )

assume A8: x = 0. R ; :: thesis: len p = len q
then len p < 1 by A2, A3, A6, Th3, XXREAL_0:1;
then A9: len p = 0 by NAT_1:14;
len q < 1 by A4, A5, A6, A8, Th3, XXREAL_0:1;
hence len p = len q by A9, NAT_1:14; :: thesis: verum

end;

A10: 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 A3, A5; :: thesis: verum

end;

now :: thesis: ( x <> 0. R implies len p = len q )

assume A11: x <> 0. R ; :: thesis: len p = len q
then len p = 1 by A2, A3, A6, Th1, NAT_1:8;
hence len p = len q by A4, A5, A6, A11, Th1, NAT_1:8; :: thesis: verum

end;

hence p = q by A7, A10, Th4; :: thesis: verum