let R be domRing; :: thesis: for a being Element of R holds LC (a | R) = a
let a be Element of R; :: thesis: LC (a | R) = a
thus LC (a | R) = LC (a * (1_. R)) by RING_4:16
.= a * (LC (1_. R)) by prl0a
.= a * (1. R) by RATFUNC1:def 7
.= a ; :: thesis: verum