let p, q be AlgSequence of R; ( 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
; p = q
A6:
1 = 0 + 1
;
A7:
now ( x = 0. R implies len p = len q )assume A8:
x = 0. R
;
len p = len qthen
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;
verum end;
A10:
for k being Nat st k < len p holds
p . k = q . k
hence
p = q
by A7, A10, Th4; verum