let c, z be Complex; :: thesis: c + <*z*> = <*(c + z)*>
A1: len <*z*> = 1 by FINSEQ_1:39;
A2: len <*(c + z)*> = 1 by FINSEQ_1:39;
A3: len (c + <*z*>) = len <*z*> by CARD_1:def 7;
thus len (c + <*z*>) = len <*(c + z)*> by A1, A2, CARD_1:def 7; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (c + <*z*>) or (c + <*z*>) . b₁ = <*(c + z)*> . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (c + <*z*>) or (c + <*z*>) . k = <*(c + z)*> . k )
assume A4: ( 1 <= k & k <= len (c + <*z*>) ) ; :: thesis: (c + <*z*>) . k = <*(c + z)*> . k
A5: k = 1 by A1, A3, A4, XXREAL_0:1;
k in dom (c + <*z*>) by A4, FINSEQ_3:25;
hence (c + <*z*>) . k = c + (<*z*> . k) by VALUED_1:def 2
.= <*(c + z)*> . k by A5 ;
:: thesis: verum