let f, g be Homomorphism of Chains (k + 1),G, Chains k,G; :: 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' ) & ( for A being Element of (Chains (k + 1),G)
for A' being Chain of (k + 1),G st A = A' holds
g . A = del A' ) implies f = g )
assume A2: 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' ; :: thesis: ( ex A being Element of (Chains (k + 1),G) ex A' being Chain of (k + 1),G st
( A = A' & not g . A = del A' ) or f = g )
assume A3: for A being Element of (Chains (k + 1),G)
for A' being Chain of (k + 1),G st A = A' holds
g . A = del A' ; :: thesis: f = g

now

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

end;

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