let G be Group; :: thesis: for H being Subgroup of G holds
( incl (H,G) is one-to-one & Image (incl (H,G)) = multMagma(# the carrier of H, the multF of H #) )
let H be Subgroup of G; :: thesis: ( incl (H,G) is one-to-one & Image (incl (H,G)) = multMagma(# the carrier of H, the multF of H #) )
set f = incl (H,G);
A1: incl (H,G) = id the carrier of H by Def9;
then A2: the carrier of H = rng (incl (H,G))
.= the carrier of (Image (incl (H,G))) by GROUP_6:44 ;
Ker (incl (H,G)) = (1). H

proof

for h being Element of H holds
( h in Ker (incl (H,G)) iff h in (1). H )

proof

let h be Element of H; :: thesis: ( h in Ker (incl (H,G)) iff h in (1). H )

hereby :: thesis: ( h in (1). H implies h in Ker (incl (H,G)) )

assume h in Ker (incl (H,G)) ; :: thesis: h in (1). H
then (incl (H,G)) . h = 1_ G by GROUP_6:41
.= 1_ H by GROUP_2:44 ;
then h in {(1_ H)} by A1, TARSKI:def 1;
hence h in (1). H by GROUP_2:def 7; :: thesis: verum

end;

assume h in (1). H ; :: thesis: h in Ker (incl (H,G))
then h in {(1_ H)} by GROUP_2:def 7;
then h = 1_ H by TARSKI:def 1;
then (incl (H,G)) . h = 1_ G by GROUP_6:31;
hence h in Ker (incl (H,G)) by GROUP_6:41; :: thesis: verum

end;

hence Ker (incl (H,G)) = (1). H by GROUP_2:def 6; :: thesis: verum

end;

hence incl (H,G) is one-to-one by GROUP_6:56; :: thesis: Image (incl (H,G)) = multMagma(# the carrier of H, the multF of H #)
thus Image (incl (H,G)) = multMagma(# the carrier of H, the multF of H #) by A2, GROUP_2:59; :: thesis: verum