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