let f1, f2 be Relation of (Seg n); :: thesis: ( ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f1,i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f2,i) = {i} ) ) ) implies f1 = f2 )
assume that
A24: for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f1,i) = {i} ) ) and
A25: for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f2,i) = {i} ) ) ; :: 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 A26: x in Seg n ; :: thesis: Im (f1,x) = Im (f2,x)
then reconsider i2 = x as Element of NAT ;
A27: ( 1 <= i2 & i2 <= n ) by A26, FINSEQ_1:1;
per cases ( ( 1 < i2 & i2 < n ) or ( i2 = 1 & i2 < n ) or ( 1 < i2 & i2 = n ) or ( i2 = 1 & i2 = n ) ) by A27, XXREAL_0:1;
suppose A28: ( 1 < i2 & i2 < n ) ; :: thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2,(i2 -' 1),(i2 + 1)};
Im (f1,x) = {i2,(i2 -' 1),(i2 + 1)} by A24, A26, A28;
hence Im (f1,x) = Im (f2,x) by A25, A26, A28; :: thesis: verum
end;
suppose A29: ( i2 = 1 & i2 < n ) ; :: thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2,n,(i2 + 1)};
Im (f1,x) = {i2,n,(i2 + 1)} by A24, A26, A29;
hence Im (f1,x) = Im (f2,x) by A25, A26, A29; :: thesis: verum
end;
suppose A30: ( 1 < i2 & i2 = n ) ; :: thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2,(i2 -' 1),1};
Im (f1,x) = {i2,(i2 -' 1),1} by A24, A26, A30;
hence Im (f1,x) = Im (f2,x) by A25, A26, A30; :: thesis: verum
end;
suppose A31: ( i2 = 1 & i2 = n ) ; :: thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2};
Im (f1,x) = {i2} by A24, A26, A31;
hence Im (f1,x) = Im (f2,x) by A25, A26, A31; :: thesis: verum
end;
end;
end;
hence f1 = f2 by RELSET_1:31; :: thesis: verum