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