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

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