Description: Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019)