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 A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) & the carrier of C2 = bool (cells k,G) & 0. C2 = 0_ k,G & ( for A, B being Element of C2
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) 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 C1
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 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 C2
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ; :: 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 A9, B9 being Chain of k,G such that
A13: AB = [A9,B9] by DOMAIN_1:9;
reconsider A1 = A9, B1 = B9 as Element of C1 by A7;
reconsider A2 = A9, B2 = B9 as Element of C2 by A10;
thus op1 . AB = A1 + B1 by A13
.= A9 + B9 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