let c be FinSequence of COMPLEX ; :: thesis: for n being Nat st n in dom (Im c) holds
(Im c) . n = Im (c . n)
let n be Nat; :: thesis: ( n in dom (Im c) implies (Im c) . n = Im (c . n) )
assume n in dom (Im c) ; :: thesis: (Im c) . n = Im (c . n)
then ( 1 <= n & n <= len (Im 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) * <i> )) * (c - (c *' )) = ((- ((1 / 2) * <i> )) * c) - ((- ((1 / 2) * <i> )) * (c *' )) by COMPLSP2:43;
( len ((- ((1 / 2) * <i> )) * c) = len c & len ((- ((1 / 2) * <i> )) * (c *' )) = len (c *' ) ) by COMPLSP2:3;
then len ((- ((1 / 2) * <i> )) * c) = len ((- ((1 / 2) * <i> )) * (c *' )) by COMPLSP2:def 1;
then A4: (Im c) . n = (((- ((1 / 2) * <i> )) * c) . n) - (((- ((1 / 2) * <i> )) * (c *' )) . n) by A3, A2, COMPLSP2:25;
((- ((1 / 2) * <i> )) * (c *' )) . n = (- ((1 / 2) * <i> )) * ((c *' ) . n) by COMPLSP2:16
.= (- ((1 / 2) * <i> )) * ((c . n) *' ) by A1, COMPLSP2:def 1 ;
then A5: (Im c) . n = ((- ((1 / 2) * <i> )) * (c . n)) - ((- ((1 / 2) * <i> )) * ((c . n) *' )) by A4, COMPLSP2:16;
(c . n) - ((c . n) *' ) = ((Re (c . n)) + ((Im (c . n)) * <i> )) - ((Re (c . n)) - ((Im (c . n)) * <i> )) by COMPLEX1:29;
hence (Im c) . n = Im (c . n) by A5; :: thesis: verum