let f, g be Homomorphism of Chains (k + 1),G, Chains k,G; :: thesis: ( ( for A being Element of (Chains (k + 1),G)
for A9 being Chain of (k + 1),G st A = A9 holds
f . A = del A9 ) & ( for A being Element of (Chains (k + 1),G)
for A9 being Chain of (k + 1),G st A = A9 holds
g . A = del A9 ) implies f = g )
assume A3: for A being Element of (Chains (k + 1),G)
for A9 being Chain of (k + 1),G st A = A9 holds
f . A = del A9 ; :: thesis: ( ex A being Element of (Chains (k + 1),G) ex A9 being Chain of (k + 1),G st
( A = A9 & not g . A = del A9 ) or f = g )
assume A4: for A being Element of (Chains (k + 1),G)
for A9 being Chain of (k + 1),G st A = A9 holds
g . A = del A9 ; :: thesis: f = g

now

let A be Element of (Chains (k + 1),G); :: thesis: f . A = g . A
reconsider A9 = A as Element of (Chains (k + 1),G) ;
reconsider A99 = A as Chain of (k + 1),G by Def17;
f . A9 = del A99 by A3
.= g . A9 by A4 ;
hence f . A = g . A ; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum