let G be addGroup; :: thesis: for H being Subgroup of G holds add_inverse H = (add_inverse G) | the carrier of H
let H be Subgroup of G; :: thesis: add_inverse H = (add_inverse G) | the carrier of H
A1: the carrier of G /\ the carrier of H = the carrier of H by DefA5, XBOOLE_1:28;

A2: now :: thesis: for x being object st x in dom (add_inverse H) holds
(add_inverse H) . x = (add_inverse G) . x

let x be object ; :: thesis: ( x in dom (add_inverse H) implies (add_inverse H) . x = (add_inverse G) . x )
assume x in dom (add_inverse H) ; :: thesis: (add_inverse H) . x = (add_inverse G) . x
then reconsider a = x as Element of H ;
reconsider b = a as Element of G by Th41, STRUCT_0:def 5;
thus (add_inverse H) . x = - a by Def6
.= - b by Th48
.= (add_inverse G) . x by Def6 ; :: thesis: verum

end;

( dom (add_inverse H) = the carrier of H & dom (add_inverse G) = the carrier of G ) by FUNCT_2:def 1;
hence add_inverse H = (add_inverse G) | the carrier of H by A1, A2, FUNCT_1:46; :: thesis: verum