let i, n be Nat; :: thesis: for c being Complex
for g1 being n -element complex-valued FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
let c be Complex; :: thesis: for g1 being n -element complex-valued FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
let g1 be n -element complex-valued 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;
A2: dom (0* n) = Seg n ;
A3: dom g1 = Seg n by FINSEQ_1:89;
A4: dom (g1 +* (i,c)) = dom g1 by FUNCT_7:30;
hence dom ((g1 +* (i,c)) - g1) = dom ((0* n) +* (i,(c - (g1 . i)))) by A1, A3, FINSEQ_1:89; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom ((g1 +* (i,c)) - g1) or ((g1 +* (i,c)) - g1) . b1 = ((0* n) +* (i,(c - (g1 . i)))) . b1 )
let x be object ; :: thesis: ( not x in dom ((g1 +* (i,c)) - g1) or ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x )
assume A5: x in dom ((g1 +* (i,c)) - g1) ; :: thesis: ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x
then A6: ((g1 +* (i,c)) - g1) . x = ((g1 +* (i,c)) . x) - (g1 . x) by VALUED_1:13;
per cases ( x = i or x <> i ) ;
suppose A7: 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 A6, A1, A5, A4, FUNCT_7:31
.= ((0* n) +* (i,(c - (g1 . i)))) . x by A1, A2, A3, A5, A4, A7, FUNCT_7:31 ;
:: thesis: verum
end;
suppose A8: 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 A6, FUNCT_7:32
.= (n |-> 0) . x
.= ((0* n) +* (i,(c - (g1 . i)))) . x by A8, FUNCT_7:32 ;
:: thesis: verum
end;
end;