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 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} ) ) ) & ( 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 A25: x in Seg n ; :: thesis: Im f1,x = Im f2,x
then reconsider i2 = x as Element of NAT ;
A26: ( 1 <= i2 & i2 <= n ) by A25, FINSEQ_1:3;

per cases ( ( 1 < i2 & i2 < n ) or ( i2 = 1 & i2 < n ) or ( 1 < i2 & i2 = n ) or ( i2 = 1 & i2 = n ) ) by A26, XXREAL_0:1;

suppose A27: ( 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, A25, A27;
hence Im f1,x = Im f2,x by A24, A25, A27; :: thesis: verum

end;

suppose A28: ( 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, A25, A28;
hence Im f1,x = Im f2,x by A24, A25, A28; :: thesis: verum

end;

suppose A29: ( 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, A25, A29;
hence Im f1,x = Im f2,x by A24, A25, A29; :: thesis: verum

end;

suppose A30: ( i2 = 1 & i2 = n ) ; :: thesis: Im f1,x = Im f2,x

set y0 = {i2};
Im f1,x = {i2} by A24, A25, A30;
hence Im f1,x = Im f2,x by A24, A25, A30; :: thesis: verum

end;

end;

end;

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