let G1, G2 be Group; :: thesis: for f being Function of the carrier of G1,the carrier of G2
for A being Subset of G1 holds f .: A c= f .: the carrier of (gr A)
let f be Function of the carrier of G1,the carrier of G2; :: thesis: for A being Subset of G1 holds f .: A c= f .: the carrier of (gr A)
let A be Subset of G1; :: thesis: f .: A c= f .: the carrier of (gr A)
A c= the carrier of (gr A) by GROUP_4:def 5;
hence f .: A c= f .: the carrier of (gr A) by RELAT_1:156; :: thesis: verum