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

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