let C1, C2 be strict AbGroup; :: thesis: ( the carrier of C1 = bool (cells k,G) & 0. C1 = 0_ k,G & ( for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) & the carrier of C2 = bool (cells k,G) & 0. C2 = 0_ k,G & ( for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) implies C1 = C2 )
assume that
A7: the carrier of C1 = bool (cells k,G) and
A8: 0. C1 = 0_ k,G and
A9: for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' and
A10: the carrier of C2 = bool (cells k,G) and
A11: 0. C2 = 0_ k,G and
A12: for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ; :: thesis: C1 = C2
set X = [:(bool (cells k,G)),(bool (cells k,G)):];
reconsider op1 = the addF of C1, op2 = the addF of C2 as Function of [:(bool (cells k,G)),(bool (cells k,G)):], bool (cells k,G) by A7, A10;

now

let AB be Element of [:(bool (cells k,G)),(bool (cells k,G)):]; :: thesis: op1 . AB = op2 . AB
consider A', B' being Chain of k,G such that
A13: AB = [A',B'] by DOMAIN_1:9;
reconsider A1 = A', B1 = B' as Element of by A7;
reconsider A2 = A', B2 = B' as Element of by A10;
thus op1 . AB = A1 + B1 by A13
.= A' + B' by A9
.= A2 + B2 by A12
.= op2 . AB by A13 ; :: thesis: verum

end;

hence C1 = C2 by A7, A8, A10, A11, FUNCT_2:113; :: thesis: verum