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: verumproof
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 A11:
( ( 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)} ) )
;
:: 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 A11, A12;
hence
Im f1,
x = Im f2,
x
by A11, A12;
:: thesis: verum
end;
hence
f1 = f2
by RELSET_1:54;
:: thesis: verum
end;