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 :: thesis: for A being Element of (Chains ((k + 1),G)) holds f . A = g . A
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 Def16;
f . A9 = del A99 by A3
.= g . A9 by A4 ;
hence f . A = g . A ; :: thesis: verum
end;
hence f = g by FUNCT_2:63; :: thesis: verum