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 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 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 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 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)

for i, j being 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 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 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 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

hence
f1 = f2
by RELSET_1:31; :: thesis: verum
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 object 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 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;assume A18: x in [:(Seg n),(Seg m):] ; :: thesis: Im (f1,x) = Im (f2,x)

then consider u, y being object 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 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