let M be non empty right_unital associative multLoopStr ; :: thesis: for u, v being unital Element of M holds u * v is unital
let u, v be unital Element of M; :: thesis: u * v is unital
consider a being Element of M such that
A1: ( u * a = 1. M & a * u = 1. M ) by GCD_1:def 2;
consider b being Element of M such that
A2: ( v * b = 1. M & b * v = 1. M ) by GCD_1:def 2;
A3: (u * v) * (b * a) = u * (v * (b * a)) by GROUP_1:def 3
.= u * ((1. M) * a) by A2, GROUP_1:def 3
.= (u * (1. M)) * a by GROUP_1:def 3
.= 1. M by A1 ;
(b * a) * (u * v) = ((b * a) * u) * v by GROUP_1:def 3
.= (b * (1. M)) * v by A1, GROUP_1:def 3
.= 1. M by A2 ;
hence u * v is unital by A3, GCD_1:def 2; :: thesis: verum