let n be Nat; :: thesis: for c1, c2 being Complex holds c1 + (n |-> c2) = n |-> (c1 + c2)
let c1, c2 be Complex; :: thesis: c1 + (n |-> c2) = n |-> (c1 + c2)
A1: ( len (c1 + (n |-> c2)) = len (n |-> c2) & len (n |-> c2) = n & n = len (n |-> (c1 + c2)) ) by CARD_1:def 7;
now :: thesis: for i being Nat st 1 <= i & i <= n holds
(n |-> (c1 + c2)) . i = (c1 + (n |-> c2)) . i
let i be Nat; :: thesis: ( 1 <= i & i <= n implies (n |-> (c1 + c2)) . i = (c1 + (n |-> c2)) . i )
assume A2: ( 1 <= i & i <= n ) ; :: thesis: (n |-> (c1 + c2)) . i = (c1 + (n |-> c2)) . i
A3: i in dom (c1 + (n |-> c2)) by A2, A1, FINSEQ_3:25;
A4: i in Seg n by A2;
hence (n |-> (c1 + c2)) . i = c1 + c2 by FINSEQ_2:57
.= c1 + ((n |-> c2) . i) by A4, FINSEQ_2:57
.= (c1 + (n |-> c2)) . i by A3, VALUED_1:def 2 ;
:: thesis: verum
end;
hence c1 + (n |-> c2) = n |-> (c1 + c2) by FINSEQ_1:14, A1; :: thesis: verum