let G be Group; :: thesis: for H, K being Group st H is Subgroup of G holds
for phi being Homomorphism of G,K holds phi | the carrier of H = phi * (incl (H,G))
let H, K be Group; :: thesis: ( H is Subgroup of G implies for phi being Homomorphism of G,K holds phi | the carrier of H = phi * (incl (H,G)) )
assume A1: H is Subgroup of G ; :: thesis: for phi being Homomorphism of G,K holds phi | the carrier of H = phi * (incl (H,G))
let phi be Homomorphism of G,K; :: thesis: phi | the carrier of H = phi * (incl (H,G))
A2: dom (phi | the carrier of H) = the carrier of H

proof

dom phi = the carrier of G by FUNCT_2:def 1;
hence dom (phi | the carrier of H) = the carrier of H by A1, GROUP_2:def 5, RELAT_1:62; :: thesis: verum

end;

for x being object st x in dom (phi | the carrier of H) holds
(phi | the carrier of H) . x = (phi * (incl (H,G))) . x

proof

let x be object ; :: thesis: ( x in dom (phi | the carrier of H) implies (phi | the carrier of H) . x = (phi * (incl (H,G))) . x )
assume B1: x in dom (phi | the carrier of H) ; :: thesis: (phi | the carrier of H) . x = (phi * (incl (H,G))) . x
hence (phi * (incl (H,G))) . x = phi . ((incl (H,G)) . x) by A2, FUNCT_2:15
.= phi . x by A1, A2, B1, Th18
.= (phi | the carrier of H) . x by B1, FUNCT_1:47 ;
:: thesis: verum

end;

hence phi | the carrier of H = phi * (incl (H,G)) by A2, FUNCT_2:def 1; :: thesis: verum