let R be Skew-Field; :: thesis: for a, b being Element of R
for c, d being Element of (MultGroup R) st a = c & b = d holds
c * d = a * b
let a, b be Element of R; :: thesis: for c, d being Element of (MultGroup R) st a = c & b = d holds
c * d = a * b
let c, d be Element of (MultGroup R); :: thesis: ( a = c & b = d implies c * d = a * b )
assume A1: ( a = c & b = d ) ; :: thesis: c * d = a * b
set cMGR = the carrier of (MultGroup R);
A2: [c,d] in [: the carrier of (MultGroup R), the carrier of (MultGroup R):] by ZFMISC_1:def 2;
thus c * d = ( the multF of R || the carrier of (MultGroup R)) . (c,d) by Def1
.= a * b by A1, A2, FUNCT_1:49 ; :: thesis: verum