let n be Nat; :: thesis: abs (1* n) = n |-> 1
thus abs (1* n) = n |-> (absreal . 1) by FINSEQOP:16
.= n |-> (abs 1) by Def2
.= n |-> 1 by ABSVALUE:def 1 ; :: thesis: verum