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

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