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
verumproof
let f1,
f2 be
Relation of
(Seg n);
( ( 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))}
;
f1 = f2
for
x being
set st
x in Seg n holds
Im (
f1,
x)
= Im (
f2,
x)
proof
let x be
set ;
( x in Seg n implies Im (f1,x) = Im (f2,x) )
assume A12:
x in Seg n
;
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;
verum
end;
hence
f1 = f2
by RELSET_1:31;
verum
end;