let f be FinSequence of COMPLEX ; :: thesis: for x being Complex holds f + x = f + ((len f) |-> x)
let x be Complex; :: thesis: f + x = f + ((len f) |-> x)
reconsider g = (len f) |-> x as FinSequence of COMPLEX by NEWTON02:103;
A0: dom (f + x) = dom f by VALUED_1:def 2;
A2: len (f + g) = min ((len f),(len ((len f) |-> x))) by FLS
.= len f ;
for i being Nat st i in dom (f + x) holds
(f + x) . i = (f + g) . i
proof
let i be Nat; :: thesis: ( i in dom (f + x) implies (f + x) . i = (f + g) . i )
assume B1: i in dom (f + x) ; :: thesis: (f + x) . i = (f + g) . i
B2: i in dom f by B1, VALUED_1:def 2;
reconsider i = i as non zero Nat by B1, FINSEQ_3:25;
len f >= i by B2, FINSEQ_3:25;
then reconsider k = (len f) - i as Element of NAT by NAT_1:21;
i in dom (f + g) by A2, B2, FINSEQ_3:29;
then (f + g) . i = (f . i) + (((k + i) |-> x) . i) by VALUED_1:def 1
.= (f . i) + x ;
hence (f + x) . i = (f + g) . i by B1, VALUED_1:def 2; :: thesis: verum
end;
hence f + x = f + ((len f) |-> x) by A0, FINSEQ_3:29, A2, FINSEQ_2:9; :: thesis: verum