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 ) ;

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

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

end;

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

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

end;

end;