let k be Nat; :: thesis: for D being non empty set holds (<*> D) /^ k = <*> D
let D be non empty set ; :: thesis: (<*> D) /^ k = <*> D

per cases ( k = 0 or k > 0 ) by NAT_1:3;

suppose k = 0 ; :: thesis: (<*> D) /^ k = <*> D

hence (<*> D) /^ k = <*> D by FINSEQ_5:31; :: thesis: verum

end;

suppose k > 0 ; :: thesis: (<*> D) /^ k = <*> D

then k > len (<*> D) ;
hence (<*> D) /^ k = <*> D by RFINSEQ:def 2; :: thesis: verum

end;

end;