let i, n be Nat; :: thesis: ( ChangeVal_2 (i,n) = 1 implies i = 1 )
assume A1: ChangeVal_2 (i,n) = 1 ; :: thesis: i = 1
assume A2: i <> 1 ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( i = 2 to_power n or i <> 2 to_power n ) ;

suppose i = 2 to_power n ; :: thesis: contradiction

hence contradiction by A1, Def8; :: thesis: verum

end;

suppose i <> 2 to_power n ; :: thesis: contradiction

hence contradiction by A1, A2, Def8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum