set I = Image f;
let u, v be Element of (Image f); :: according to GROUP_1:def 12 :: thesis: u * v = v * u
consider a being Element of R such that
A1: f . a = u by T6;
consider b being Element of R such that
A2: f . b = v by T6;
thus u * v = (f . b) * (f . a) by A1, A2, T5
.= v * u by A1, A2, T5 ; :: thesis: verum