let n be Element of NAT ; :: thesis: abs (1* n) = n |-> 1
thus abs (1* n) = n |-> (absreal . 1) by FINSEQOP:16
.= n |-> (abs 1) by EUCLID:def 2
.= n |-> 1 by ABSVALUE:def 1 ; :: thesis: verum