let n, m be Nat; :: thesis: ( n <> 0 implies m = (((divSeq m,n) . 0 ) * n) + ((modSeq m,n) . 0 ) )
set fd = divSeq m,n;
set fm = modSeq m,n;
assume A1: n <> 0 ; :: thesis: m = (((divSeq m,n) . 0 ) * n) + ((modSeq m,n) . 0 )
( (divSeq m,n) . 0 = m div n & (modSeq m,n) . 0 = m mod n ) by Def2, Def3;
hence m = (((divSeq m,n) . 0 ) * n) + ((modSeq m,n) . 0 ) by A1, NAT_D:2; :: thesis: verum