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 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)

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;

then f9 is additive by VECTSP_1:def 20;
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