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 C1
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 C2
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) implies C1 = C2 )
assume A5: ( the carrier of C1 = bool (cells k,G) & 0. C1 = 0_ k,G & ( for A, B being Element of C1
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 C2
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 A5;

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
A6: AB = [A',B'] by DOMAIN_1:9;
reconsider A1 = A', B1 = B' as Element of C1 by A5;
reconsider A2 = A', B2 = B' as Element of C2 by A5;
thus op1 . AB = A1 + B1 by A6
.= A' + B' by A5
.= A2 + B2 by A5
.= op2 . AB by A6 ; :: thesis: verum

end;

hence C1 = C2 by A5, FUNCT_2:113; :: thesis: verum