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