theorem Th20: :: IDEA_1:20

for n, a1, a2 being Nat st a1 <> 0 & a2 <> 0 & ChangeVal_2 (a1,n) = ChangeVal_2 (a2,n) holds
a1 = a2