let C1, C2 be strict AbGroup; ( 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
; 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;
hence
C1 = C2
by A7, A8, A10, A11, FUNCT_2:63; verum