let G1, G2 be Group; :: thesis: for H being Subgroup of G1
for f being Homomorphism of G1,G2
for h being Element of G1 st h in H holds
(f | H) . h = f . h
let H be Subgroup of G1; :: thesis: for f being Homomorphism of G1,G2
for h being Element of G1 st h in H holds
(f | H) . h = f . h
let f be Homomorphism of G1,G2; :: thesis: for h being Element of G1 st h in H holds
(f | H) . h = f . h
let h be Element of G1; :: thesis: ( h in H implies (f | H) . h = f . h )
assume h in H ; :: thesis: (f | H) . h = f . h
then (f | the carrier of H) . h = f . h by FUNCT_1:49;
hence (f | H) . h = f . h by GRSOLV_1:def 2; :: thesis: verum