thus for f1, f2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
Im (f1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (f2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds
f1 = f2 :: thesis: verum

proof

let f1, f2 be Relation of (Seg n); :: thesis: ( ( for i being Element of NAT st i in Seg n holds
Im (f1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (f2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) implies f1 = f2 )
assume that
A10: for i being Element of NAT st i in Seg n holds
Im (f1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} and
A11: for i being Element of NAT st i in Seg n holds
Im (f2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ; :: thesis: f1 = f2
for x being set st x in Seg n holds
Im (f1,x) = Im (f2,x)

proof

let x be set ; :: thesis: ( x in Seg n implies Im (f1,x) = Im (f2,x) )
assume A12: x in Seg n ; :: thesis: Im (f1,x) = Im (f2,x)
then reconsider i2 = x as Element of NAT ;
Im (f1,i2) = {i2,(max ((i2 -' 1),1)),(min ((i2 + 1),n))} by A10, A12;
hence Im (f1,x) = Im (f2,x) by A11, A12; :: thesis: verum

end;

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

end;