hereby :: thesis: ( ex t being Nat st l = k * t implies k divides l )

assume A1: k divides l ; :: thesis: ex t being Nat st l = k * t
thus ex t being Nat st l = k * t :: thesis: verum

proof

consider t being Integer such that
A2: l = k * t by A1, INT_1:def 3;

per cases ( 0 < l or l = 0 ) ;

suppose 0 < l ; :: thesis: ex t being Nat st l = k * t

then 0 <= t by A2;
then reconsider t = t as Element of NAT by INT_1:3;
take t ; :: thesis: l = k * t
thus l = k * t by A2; :: thesis: verum

end;

suppose A3: l = 0 ; :: thesis: ex t being Nat st l = k * t

take 0 ; :: thesis: l = k * 0
thus l = k * 0 by A3; :: thesis: verum

end;

end;

end;

end;

thus ( ex t being Nat st l = k * t implies k divides l ) by INT_1:def 3; :: thesis: verum