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 Def1, Def2;
hence m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0) by A1, NAT_D:2; :: thesis: verum