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