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) )
assume n in dom (Re c) ; :: thesis: (Re c) . n = Re (c . n)
then ( 1 <= n & n <= len (Re c) ) by FINSEQ_3:27;
then A1: ( 1 <= n & n <= len c ) by COMPLSP2:48;
A2: n in NAT by ORDINAL1:def 13;
len (c *' ) = len c by COMPLSP2:def 1;
then A3: (1 / 2) * (c + (c *' )) = ((1 / 2) * c) + ((1 / 2) * (c *' )) by COMPLSP2:30;
( len ((1 / 2) * c) = len c & len ((1 / 2) * (c *' )) = len (c *' ) ) by COMPLSP2:3;
then len ((1 / 2) * c) = len ((1 / 2) * (c *' )) by COMPLSP2:def 1;
then A4: (Re c) . n = (((1 / 2) * c) . n) + (((1 / 2) * (c *' )) . n) by A3, A2, COMPLSP2:26;
((1 / 2) * (c *' )) . n = (1 / 2) * ((c *' ) . n) by COMPLSP2:16;
then ((1 / 2) * (c *' )) . n = (1 / 2) * ((c . n) *' ) by A1, COMPLSP2:def 1;
then A5: (Re c) . n = ((1 / 2) * (c . n)) + ((1 / 2) * ((c . n) *' )) by A4, COMPLSP2:16;
c . n = (Re (c . n)) + ((Im (c . n)) * <i> ) by COMPLEX1:29;
hence (Re c) . n = Re (c . n) by A5; :: thesis: verum