let c be FinSequence of COMPLEX ; :: thesis: for n being Nat st n in dom (Re c) holds
(Re c) . n = Re (c . n)
let n be Nat; :: thesis: ( n in dom (Re c) implies (Re c) . n = Re (c . n) )
A1: ((1 / 2) * (c *')) . n = (1 / 2) * ((c *') . n) by COMPLSP2:16;
( len ((1 / 2) * c) = len c & len ((1 / 2) * (c *')) = len (c *') ) by COMPLSP2:3;
then A2: len ((1 / 2) * c) = len ((1 / 2) * (c *')) by COMPLSP2:def 1;
len (c *') = len c by COMPLSP2:def 1;
then ( n in NAT & (1 / 2) * (c + (c *')) = ((1 / 2) * c) + ((1 / 2) * (c *')) ) by COMPLSP2:30, ORDINAL1:def 12;
then A3: (Re c) . n = (((1 / 2) * c) . n) + (((1 / 2) * (c *')) . n) by A2, COMPLSP2:26;
assume A4: n in dom (Re c) ; :: thesis: (Re c) . n = Re (c . n)
then n <= len (Re c) by FINSEQ_3:25;
then A5: n <= len c by COMPLSP2:48;
1 <= n by A4, FINSEQ_3:25;
then ((1 / 2) * (c *')) . n = (1 / 2) * ((c . n) *') by A5, A1, COMPLSP2:def 1;
then A6: (Re c) . n = ((1 / 2) * (c . n)) + ((1 / 2) * ((c . n) *')) by A3, COMPLSP2:16;
c . n = (Re (c . n)) + ((Im (c . n)) * <i>) by COMPLEX1:13;
hence (Re c) . n = Re (c . n) by A6; :: thesis: verum