let seq be Complex_Sequence; :: thesis: for r being Real holds
( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )
let r be Real; :: thesis: ( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )

now :: thesis: for n being Element of NAT holds (r (#) (Re seq)) . n = (Re (r (#) seq)) . n

let n be Element of NAT ; :: thesis: (r (#) (Re seq)) . n = (Re (r (#) seq)) . n
thus (r (#) (Re seq)) . n = r * ((Re seq) . n) by SEQ_1:9
.= r * (Re (seq . n)) by Def5
.= Re (r * (seq . n)) by Th17
.= Re ((r (#) seq) . n) by VALUED_1:6
.= (Re (r (#) seq)) . n by Def5 ; :: thesis: verum

end;

hence r (#) (Re seq) = Re (r (#) seq) ; :: thesis: r (#) (Im seq) = Im (r (#) seq)

now :: thesis: for n being Element of NAT holds (r (#) (Im seq)) . n = (Im (r (#) seq)) . n

let n be Element of NAT ; :: thesis: (r (#) (Im seq)) . n = (Im (r (#) seq)) . n
thus (r (#) (Im seq)) . n = r * ((Im seq) . n) by SEQ_1:9
.= r * (Im (seq . n)) by Def6
.= Im (r * (seq . n)) by Th17
.= Im ((r (#) seq) . n) by VALUED_1:6
.= (Im (r (#) seq)) . n by Def6 ; :: thesis: verum

end;

hence r (#) (Im seq) = Im (r (#) seq) ; :: thesis: verum