let A, B be AbGroup; :: thesis: for i being Homomorphism of A,B st i = id A holds
A is SubAbGr of B
let i be Homomorphism of A,B; :: thesis: ( i = id A implies A is SubAbGr of B )
assume A1: i = id A ; :: thesis: A is SubAbGr of B
A2: for o being object st o in the carrier of A holds
o in the carrier of B

proof

let o be object ; :: thesis: ( o in the carrier of A implies o in the carrier of B )
assume A3: o in the carrier of A ; :: thesis: o in the carrier of B
then i . o = o by A1, FUNCT_1:18;
hence o in the carrier of B by FUNCT_2:5, A3; :: thesis: verum

end;

A5: the carrier of A c= the carrier of B by A2;
A6: the addF of A = the addF of B || the carrier of A

proof

set aA = the addF of A;
set aB = the addF of B || the carrier of A;
A7: dom ( the addF of B || the carrier of A) = (dom the addF of B) /\ [: the carrier of A, the carrier of A:] by RELAT_1:61
.= [: the carrier of B, the carrier of B:] /\ [: the carrier of A, the carrier of A:] by FUNCT_2:def 1
.= [: the carrier of A, the carrier of A:] by A5, ZFMISC_1:96, XBOOLE_1:28 ;
for x being object st x in dom the addF of A holds
the addF of A . x = ( the addF of B || the carrier of A) . x

proof

let x be object ; :: thesis: ( x in dom the addF of A implies the addF of A . x = ( the addF of B || the carrier of A) . x )
assume A8: x in dom the addF of A ; :: thesis: the addF of A . x = ( the addF of B || the carrier of A) . x
then consider a, b being object such that
A9: ( a in the carrier of A & b in the carrier of A & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of A by A9;
reconsider a1 = a, b1 = b as Element of B by A2;
A10: i . a = a by A1;
A11: i . b = b by A1;
the addF of A . x = i . (a + b) by A1, A9
.= a1 + b1 by A10, A11, VECTSP_1:def 20
.= ( the addF of B || the carrier of A) . x by A8, A9, FUNCT_1:49 ;
hence the addF of A . x = ( the addF of B || the carrier of A) . x ; :: thesis: verum

end;

hence the addF of A = the addF of B || the carrier of A by A7, FUNCT_2:def 1; :: thesis: verum

end;

0. B = i . (0. A) by MOD_4:40
.= 0. A by A1 ;
hence A is SubAbGr of B by A5, A6, Def6; :: thesis: verum