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;

hence inverse_op H = (inverse_op G) | the carrier of H by A1, A2, FUNCT_1:46; :: thesis: verum

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

( dom (inverse_op H) = the carrier of H & dom (inverse_op G) = the carrier of G )
by FUNCT_2:def 1;(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;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

hence inverse_op H = (inverse_op G) | the carrier of H by A1, A2, FUNCT_1:46; :: thesis: verum