deffunc H_{2}( Subset of (cells ((k + 1),G))) -> Cycle of k,G = del $1;

consider f being Function of (bool (cells ((k + 1),G))),(bool (cells (k,G))) such that

A1: for A being Subset of (cells ((k + 1),G)) holds f . A = H_{2}(A)
from FUNCT_2:sch 4();

A2: the carrier of (Chains ((k + 1),G)) = bool (cells ((k + 1),G)) by Def16;

the carrier of (Chains (k,G)) = bool (cells (k,G)) by Def16;

then reconsider f9 = f as Function of (Chains ((k + 1),G)),(Chains (k,G)) by A2;

then reconsider f9 = f9 as Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) ;

take f9 ; :: thesis: for A being Element of (Chains ((k + 1),G))

for A9 being Chain of (k + 1),G st A = A9 holds

f9 . A = del A9

thus for A being Element of (Chains ((k + 1),G))

for A9 being Chain of (k + 1),G st A = A9 holds

f9 . A = del A9 by A1; :: thesis: verum

consider f being Function of (bool (cells ((k + 1),G))),(bool (cells (k,G))) such that

A1: for A being Subset of (cells ((k + 1),G)) holds f . A = H

A2: the carrier of (Chains ((k + 1),G)) = bool (cells ((k + 1),G)) by Def16;

the carrier of (Chains (k,G)) = bool (cells (k,G)) by Def16;

then reconsider f9 = f as Function of (Chains ((k + 1),G)),(Chains (k,G)) by A2;

now :: thesis: for A, B being Element of (Chains ((k + 1),G)) holds f . (A + B) = (f9 . A) + (f9 . B)

then
f9 is additive
by VECTSP_1:def 20;let A, B be Element of (Chains ((k + 1),G)); :: thesis: f . (A + B) = (f9 . A) + (f9 . B)

reconsider A9 = A, B9 = B as Chain of (k + 1),G by Def16;

thus f . (A + B) = f . (A9 + B9) by Def16

.= del (A9 + B9) by A1

.= (del A9) + (del B9) by Th58

.= (del A9) + (f . B9) by A1

.= (f . A9) + (f . B9) by A1

.= (f9 . A) + (f9 . B) by Def16 ; :: thesis: verum

end;reconsider A9 = A, B9 = B as Chain of (k + 1),G by Def16;

thus f . (A + B) = f . (A9 + B9) by Def16

.= del (A9 + B9) by A1

.= (del A9) + (del B9) by Th58

.= (del A9) + (f . B9) by A1

.= (f . A9) + (f . B9) by A1

.= (f9 . A) + (f9 . B) by Def16 ; :: thesis: verum

then reconsider f9 = f9 as Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) ;

take f9 ; :: thesis: for A being Element of (Chains ((k + 1),G))

for A9 being Chain of (k + 1),G st A = A9 holds

f9 . A = del A9

thus for A being Element of (Chains ((k + 1),G))

for A9 being Chain of (k + 1),G st A = A9 holds

f9 . A = del A9 by A1; :: thesis: verum