deffunc H₂( 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₂(A) from FUNCT_2:sch 4();
A2: the carrier of (Chains (k + 1),G) = bool (cells (k + 1),G) by Def17;
the carrier of (Chains k,G) = bool (cells k,G) by Def17;
then reconsider f9 = f as Function of (Chains (k + 1),G),(Chains k,G) by A2;

now

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 Def17;
thus f . (A + B) = f . (A9 + B9) by Def17
.= del (A9 + B9) by A1
.= (del A9) + (del B9) by Th63
.= (del A9) + (f . B9) by A1
.= (f . A9) + (f . B9) by A1
.= (f9 . A) + (f9 . B) by Def17 ; :: thesis: verum

end;

then reconsider f9 = f9 as Homomorphism of Chains (k + 1),G, Chains k,G by MOD_4:def 19;
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