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:25;
n <= len (Im c) by A1, FINSEQ_3:25;
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 12;
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:13;
hence (Im c) . n = Im (c . n) by A6; :: thesis: verum