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;

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

hence
c1 + (n |-> c2) = n |-> (c1 + c2)
by FINSEQ_1:14, A1; :: thesis: verum(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;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