let i be Nat; :: thesis: for D being non empty set holds (<*> D) | i = <*> D
let D be non empty set ; :: thesis: (<*> D) | i = <*> D
len (<*> D) = 0 ;
hence (<*> D) | i = <*> D by FINSEQ_1:58; :: thesis: verum