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

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

hence
f = g
by FUNCT_2:63; :: thesis: verumlet 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;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