let G be Group; :: thesis: id the carrier of G is multiplicative
set f = id the carrier of G;
let a be Element of G; :: according to GROUP_6:def 6 :: thesis: for b being Element of G holds (id the carrier of G) . (a * b) = ((id the carrier of G) . a) * ((id the carrier of G) . b)
let b be Element of G; :: thesis: (id the carrier of G) . (a * b) = ((id the carrier of G) . a) * ((id the carrier of G) . b)
thus (id the carrier of G) . (a * b) = a * b by FUNCT_1:18
.= ((id the carrier of G) . a) * b by FUNCT_1:18
.= ((id the carrier of G) . a) * ((id the carrier of G) . b) by FUNCT_1:18 ; :: thesis: verum