let G be Group; :: thesis: for H being Subgroup of G
for a1, a2 being Element of H
for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2
let H be Subgroup of G; :: thesis: for a1, a2 being Element of H
for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2
let a1, a2 be Element of H; :: thesis: for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2
A1: the carrier of H c= the carrier of G by GROUP_2:def 5;
let b1, b2 be Element of G; :: thesis: ( a1 = b1 & a2 = b2 implies a1 * a2 = b1 * b2 )
assume that
A2: a1 = b1 and
A3: a2 = b2 ; :: thesis: a1 * a2 = b1 * b2
dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def 1;
then A4: the multF of G is ManySortedSet of [: the carrier of G, the carrier of G:] by PARTFUN1:def 2;
the multF of H = the multF of G || the carrier of H by GROUP_2:def 5;
hence a1 * a2 = b1 * b2 by A1, A2, A3, A4, ALTCAT_1:5; :: thesis: verum