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();
( the carrier of (Chains (k + 1),G) = bool (cells (k + 1),G) & the carrier of (Chains k,G) = bool (cells k,G) ) by Def17;
then reconsider f' = f as Function of (Chains (k + 1),G),(Chains k,G) ;

now

let A, B be Element of (Chains (k + 1),G); :: thesis: f . (A + B) = (f' . A) + (f' . B)
reconsider A' = A, B' = B as Chain of (k + 1),G by Def17;
thus f . (A + B) = f . (A' + B') by Def17
.= del (A' + B') by A1
.= (del A') + (del B') by Th63
.= (del A') + (f . B') by A1
.= (f . A') + (f . B') by A1
.= (f' . A) + (f' . B) by Def17 ; :: thesis: verum

end;

then reconsider f' = f' as Homomorphism of Chains (k + 1),G, Chains k,G by MOD_4:def 19;
take f' ; :: thesis: for A being Element of (Chains (k + 1),G)
for A' being Chain of (k + 1),G st A = A' holds
f' . A = del A'
thus for A being Element of (Chains (k + 1),G)
for A' being Chain of (k + 1),G st A = A' holds
f' . A = del A' by A1; :: thesis: verum