let f1, f2 be Relation of [:(Seg n),(Seg m):]; :: thesis: ( ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im f1,x = [:{i},(Im (Nbdl1 m),j):] \/ [:(Im (Nbdl1 n),i),{j}:] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im f2,x = [:{i},(Im (Nbdl1 m),j):] \/ [:(Im (Nbdl1 n),i),{j}:] ) implies f1 = f2 )
assume that
A16: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im f1,x = [:{i},(Im (Nbdl1 m),j):] \/ [:(Im (Nbdl1 n),i),{j}:] and
A17: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im f2,x = [:{i},(Im (Nbdl1 m),j):] \/ [:(Im (Nbdl1 n),i),{j}:] ; :: thesis: f1 = f2
for x being set st x in [:(Seg n),(Seg m):] holds
Im f1,x = Im f2,x

proof

let x be set ; :: thesis: ( x in [:(Seg n),(Seg m):] implies Im f1,x = Im f2,x )
assume A18: x in [:(Seg n),(Seg m):] ; :: thesis: Im f1,x = Im f2,x
then consider u, y being set such that
A19: ( u in Seg n & y in Seg m ) and
A20: x = [u,y] by ZFMISC_1:def 2;
reconsider i = u, j = y as Element of NAT by A19;
Im f1,x = [:{i},(Im (Nbdl1 m),j):] \/ [:(Im (Nbdl1 n),u),{j}:] by A16, A18, A20;
hence Im f1,x = Im f2,x by A17, A18, A20; :: thesis: verum

end;

hence f1 = f2 by RELSET_1:54; :: thesis: verum