let G be Group; :: thesis: for H being Subgroup of G holds inverse_op H = (inverse_op G) | the carrier of H
let H be Subgroup of G; :: thesis: inverse_op H = (inverse_op G) | the carrier of H
the carrier of H c= the carrier of G by Def5;
then A1: the carrier of G /\ the carrier of H = the carrier of H by XBOOLE_1:28;
A2: now :: thesis: for x being object st x in dom (inverse_op H) holds
(inverse_op H) . x = (inverse_op G) . x
let x be object ; :: thesis: ( x in dom (inverse_op H) implies (inverse_op H) . x = (inverse_op G) . x )
assume x in dom (inverse_op H) ; :: thesis: (inverse_op H) . x = (inverse_op G) . x
then reconsider a = x as Element of H ;
reconsider b = a as Element of G by Th42;
thus (inverse_op H) . x = a " by GROUP_1:def 6
.= b " by Th48
.= (inverse_op G) . x by GROUP_1:def 6 ; :: thesis: verum
end;
( dom (inverse_op H) = the carrier of H & dom (inverse_op G) = the carrier of G ) by FUNCT_2:def 1;
hence inverse_op H = (inverse_op G) | the carrier of H by A1, A2, FUNCT_1:46; :: thesis: verum