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 13;
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:27;
then A5: n <= len c by COMPLSP2:48;
1 <= n by A4, FINSEQ_3:27;
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:29;
hence (Re c) . n = Re (c . n) by A6; :: thesis: verum