let X be non empty set ; :: thesis: for D being set
for F being Functional_Sequence of X,COMPLEX holds Re (F || D) = (Re F) || D
let D be set ; :: thesis: for F being Functional_Sequence of X,COMPLEX holds Re (F || D) = (Re F) || D
let F be Functional_Sequence of X,COMPLEX; :: thesis: Re (F || D) = (Re F) || D
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (Re (F || D)) . n = ((Re F) || D) . n
(Re (F || D)) . n = ((Re F) . n) | D by Lm1;
hence (Re (F || D)) . n = ((Re F) || D) . n by Def1; :: thesis: verum