let i, n be Nat; :: thesis: for c being complex number
for g1 being complex-valued n -long FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
let c be complex number ; :: thesis: for g1 being complex-valued n -long FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
let g1 be complex-valued n -long FinSequence; :: thesis: (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
A1: dom ((g1 +* (i,c)) - g1) = (dom (g1 +* (i,c))) /\ (dom g1) by VALUED_1:12;
A3: dom (0* n) = Seg n by EUCLID:3;
A4: dom g1 = Seg n by EUCLID:3;
A5: dom (g1 +* (i,c)) = dom g1 by FUNCT_7:32;
hence dom ((g1 +* (i,c)) - g1) = dom ((0* n) +* (i,(c - (g1 . i)))) by A1, A4, EUCLID:3; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((g1 +* (i,c)) - g1) or ((g1 +* (i,c)) - g1) . b₁ = ((0* n) +* (i,(c - (g1 . i)))) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((g1 +* (i,c)) - g1) or ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x )
assume A6: x in dom ((g1 +* (i,c)) - g1) ; :: thesis: ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x
then A7: ((g1 +* (i,c)) - g1) . x = ((g1 +* (i,c)) . x) - (g1 . x) by VALUED_1:13;

per cases ( x = i or x <> i ) ;

suppose A8: x = i ; :: thesis: ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x

hence ((g1 +* (i,c)) - g1) . x = c - (g1 . x) by A7, A1, A6, A5, FUNCT_7:33
.= ((0* n) +* (i,(c - (g1 . i)))) . x by A1, A3, A4, A6, A5, A8, FUNCT_7:33 ;
:: thesis: verum

end;

suppose A9: x <> i ; :: thesis: ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x

hence ((g1 +* (i,c)) - g1) . x = (g1 . x) - (g1 . x) by A7, FUNCT_7:34
.= (n |-> 0) . x
.= ((0* n) +* (i,(c - (g1 . i)))) . x by A9, FUNCT_7:34 ;
:: thesis: verum

end;

end;