let X be non empty set ; :: thesis: for D being set
for F being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
let D be set ; :: thesis: for F being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
let F be Functional_Sequence of X,COMPLEX; :: thesis: for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
set G = F || D;
let n be Nat; :: thesis: ( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
Re ((F . n) | D) = (Re (F . n)) | D by Th20;
then A1: Re ((F . n) | D) = ((Re F) . n) | D by MESFUN7C:24;
Im ((F . n) | D) = (Im (F . n)) | D by Th20;
then A2: Im ((F . n) | D) = ((Im F) . n) | D by MESFUN7C:24;
( Re ((F || D) . n) = (Re (F || D)) . n & Im ((F || D) . n) = (Im (F || D)) . n ) by MESFUN7C:24;
hence ( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D ) by A1, A2, Def1; :: thesis: verum