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 ;

p . k = q . k

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 )

A10:
for k being Nat st k < len p holds 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;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

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;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

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

hence
p = q
by A7, A10, Th4; :: thesis: verumassume 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;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