for n1, n2 being Nat holds (0* n1) ^ (0* n2) = 0* (n1 + n2) by FINSEQ_2:123;