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 A2: ( a1 = b1 & 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 A3: the multF of G is ManySortedSet of by PARTFUN1:def 4;
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, ALTCAT_1:7; :: thesis: verum