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

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