let G1, G2 be Group; :: thesis: for f being Homomorphism of G1,G2 st ( for g being Element of G1 holds f . g = g ) holds
G1 is Subgroup of G2
let f be Homomorphism of G1,G2; :: thesis: ( ( for g being Element of G1 holds f . g = g ) implies G1 is Subgroup of G2 )
assume A1: for g being Element of G1 holds f . g = g ; :: thesis: G1 is Subgroup of G2
A2: the carrier of G1 c= the carrier of G2

proof

for g being object st g in the carrier of G1 holds
g in the carrier of G2

proof

let g be object ; :: thesis: ( g in the carrier of G1 implies g in the carrier of G2 )
assume g in the carrier of G1 ; :: thesis: g in the carrier of G2
then reconsider gg = g as Element of G1 ;
f . gg in the carrier of G2 ;
hence g in the carrier of G2 by A1; :: thesis: verum

end;

hence the carrier of G1 c= the carrier of G2 by TARSKI:def 3; :: thesis: verum

end;

then reconsider U = the carrier of G1 as Subset of the carrier of G2 ;
set U1 = the carrier of G1;
set U2 = the carrier of G2;
A3: [: the carrier of G1, the carrier of G1:] c= [: the carrier of G2, the carrier of G2:] by A2, ZFMISC_1:96;
dom the multF of G2 = [: the carrier of G2, the carrier of G2:] by FUNCT_2:def 1;
then A5: dom ( the multF of G2 | [: the carrier of G1, the carrier of G1:]) = [: the carrier of G1, the carrier of G1:] by A2, ZFMISC_1:96, RELAT_1:62;
A5a: dom ( the multF of G2 || the carrier of G1) = [: the carrier of G1, the carrier of G1:] by A5, REALSET1:def 2;
A5b: the multF of G2 || the carrier of G1 = the multF of G2 | [: the carrier of G1, the carrier of G1:] by REALSET1:def 2;
A6: for a, b being Element of the carrier of G1 holds the multF of G1 . (a,b) = ( the multF of G2 || the carrier of G1) . (a,b)

proof

let a, b be Element of the carrier of G1; :: thesis: the multF of G1 . (a,b) = ( the multF of G2 || the carrier of G1) . (a,b)
B2: the multF of G2 . [a,b] = ( the multF of G2 | [: the carrier of G1, the carrier of G1:]) . [a,b] by A5, ZFMISC_1:87, FUNCT_1:47
.= ( the multF of G2 || the carrier of G1) . [a,b] by REALSET1:def 2
.= ( the multF of G2 || the carrier of G1) . (a,b) by BINOP_1:def 1 ;
set c = a * b;
B4: the multF of G2 . ((f . a),(f . b)) = the multF of G2 . ((f . a),b) by A1
.= the multF of G2 . (a,b) by A1 ;
a * b = f . (a * b) by A1
.= (f . a) * (f . b) by GROUP_6:def 6
.= the multF of G2 . (a,b) by B4 ;
hence the multF of G1 . (a,b) = ( the multF of G2 || the carrier of G1) . (a,b) by B2, BINOP_1:def 1; :: thesis: verum

end;

the multF of G2 || the carrier of G1 is BinOp of the carrier of G1

proof

B1: rng the multF of G1 c= the carrier of G1 by RELAT_1:def 19;
B2a: the multF of G2 || the carrier of G1 is Function of [: the carrier of G1, the carrier of G1:], the carrier of G2 by A3, A5b, FUNCT_2:32;
B2: the multF of G2 || the carrier of G1 is Function of [: the carrier of G1, the carrier of G1:],(rng ( the multF of G2 || the carrier of G1)) by A5a, FUNCT_2:1;
B3: rng ( the multF of G2 || the carrier of G1) c= the carrier of G1 by B1, A6, B2a, LmEqRng;
( [: the carrier of G1, the carrier of G1:] <> {} implies rng ( the multF of G2 || the carrier of G1) <> {} )

proof

assume [: the carrier of G1, the carrier of G1:] <> {} ; :: thesis: rng ( the multF of G2 || the carrier of G1) <> {}
then consider x being object such that
C2: x in [: the carrier of G1, the carrier of G1:] by XBOOLE_0:def 1;
x in dom ( the multF of G2 || the carrier of G1) by C2, A5, REALSET1:def 2;
hence rng ( the multF of G2 || the carrier of G1) <> {} by FUNCT_1:3; :: thesis: verum

end;

hence the multF of G2 || the carrier of G1 is BinOp of the carrier of G1 by B2, B3, FUNCT_2:6; :: thesis: verum

end;

hence G1 is Subgroup of G2 by A2, A6, BINOP_1:2, GROUP_2:def 5; :: thesis: verum