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;

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 :: thesis: for AB being Element of [:(bool (cells (k,G))),(bool (cells (k,G))):] holds op1 . AB = op2 . AB

hence
C1 = C2
by A7, A8, A10, A11, FUNCT_2:63; :: thesis: verumlet 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:1;

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;consider A9, B9 being Chain of k,G such that

A13: AB = [A9,B9] by DOMAIN_1:1;

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