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

(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