let G, K be Group; :: thesis: for H being Subgroup of G
for phi being Homomorphism of G,K holds phi | H = phi * (incl H)
let H be Subgroup of G; :: thesis: for phi being Homomorphism of G,K holds phi | H = phi * (incl H)
let phi be Homomorphism of G,K; :: thesis: phi | H = phi * (incl H)
for h being Element of H holds (phi | H) . h = (phi * (incl H)) . h

proof

let h be Element of H; :: thesis: (phi | H) . h = (phi * (incl H)) . h
( (incl H) . h = (id the carrier of H) . h & dom (incl H) = the carrier of H ) by Def9, FUNCT_2:def 1;
then A1: (phi * (incl H)) . h = phi . h by FUNCT_1:13;
h in G by GROUP_2:41;
then h in dom phi by FUNCT_2:def 1;
then h in (dom phi) /\ the carrier of H by XBOOLE_0:def 4;
then (phi | the carrier of H) . h = phi . h by FUNCT_1:48;
hence (phi | H) . h = (phi * (incl H)) . h by A1, GRSOLV_1:def 2; :: thesis: verum

end;

hence phi | H = phi * (incl H) by FUNCT_2:def 8; :: thesis: verum