let G, H be Group; :: thesis: for h being Element of H st H is Subgroup of G holds
(incl (H,G)) . h = h
let h be Element of H; :: thesis: ( H is Subgroup of G implies (incl (H,G)) . h = h )
assume H is Subgroup of G ; :: thesis: (incl (H,G)) . h = h
hence (incl (H,G)) . h = (id the carrier of H) . h by Def9
.= h ;
:: thesis: verum