let f1, f2 be Relation of [:(Seg n),(Seg m):]; ( ( 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) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),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) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) implies f1 = f2 )
assume that
A10:
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) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
and
A11:
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) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
; 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 ;
( x in [:(Seg n),(Seg m):] implies Im (f1,x) = Im (f2,x) )
assume A12:
x in [:(Seg n),(Seg m):]
;
Im (f1,x) = Im (f2,x)
then consider u,
y being
object such that A13:
(
u in Seg n &
y in Seg m )
and A14:
x = [u,y]
by ZFMISC_1:def 2;
reconsider i =
u,
j =
y as
Nat by A13;
Im (
f1,
x)
= [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
by A10, A12, A14;
hence
Im (
f1,
x)
= Im (
f2,
x)
by A11, A12, A14;
verum
end;
hence
f1 = f2
by RELSET_1:31; verum