deffunc H₂( Subset of ) -> 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 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 f' = f as Function of (Chains (k + 1),G),(Chains k,G) by A2;

now

let A, B be Element of ; :: 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
for A' being Chain of (k + 1),G st A = A' holds
f' . A = del A'
thus for A being Element of
for A' being Chain of (k + 1),G st A = A' holds
f' . A = del A' by A1; :: thesis: verum