let n be Nat; :: thesis: for f being finite Function
for o being valued_reorganization of f holds
( rng ((f *. o) . n) = {} or ( rng ((f *. o) . n) = {(f . (o _ (n,1)))} & 1 in dom (o . n) ) )
let f be finite Function; :: thesis: for o being valued_reorganization of f holds
( rng ((f *. o) . n) = {} or ( rng ((f *. o) . n) = {(f . (o _ (n,1)))} & 1 in dom (o . n) ) )
let o be valued_reorganization of f; :: thesis: ( rng ((f *. o) . n) = {} or ( rng ((f *. o) . n) = {(f . (o _ (n,1)))} & 1 in dom (o . n) ) )
assume rng ((f *. o) . n) <> {} ; :: thesis: ( rng ((f *. o) . n) = {(f . (o _ (n,1)))} & 1 in dom (o . n) )
then consider y being object such that
A1: y in rng ((f *. o) . n) by XBOOLE_0:def 1;
consider x being object such that
A2: ( x in dom ((f *. o) . n) & ((f *. o) . n) . x = y ) by A1, FUNCT_1:def 3;
reconsider x = x as Nat by A2;
A3: dom (f *. o) = dom o by FOMODEL2:def 6;
n in dom (f *. o)

proof

assume not n in dom (f *. o) ; :: thesis: contradiction
then (f *. o) . n = {} by FUNCT_1:def 2;
hence contradiction by A1; :: thesis: verum

end;

then (f *. o) . n = f * (o . n) by A3, FOMODEL2:def 6;
then A4: ( (f * (o . n)) . x = f . ((o . n) . x) & x in dom (o . n) ) by A2, FUNCT_1:11, FUNCT_1:12;
consider w being object such that
A5: w = f . (o _ (n,1)) & ... & w = f . (o _ (n,(len (o . n)))) by Def9;
( 1 <= x & x <= len (o . n) ) by A4, FINSEQ_3:25;
then A6: ( w = f . (o _ (n,x)) & 1 <= len (o . n) ) by XXREAL_0:2, A5;
rng ((f *. o) . n) c= {(f . (o _ (n,1)))}

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng ((f *. o) . n) or z in {(f . (o _ (n,1)))} )
assume A7: z in rng ((f *. o) . n) ; :: thesis: z in {(f . (o _ (n,1)))}
then consider x being object such that
A8: ( x in dom ((f *. o) . n) & ((f *. o) . n) . x = z ) by FUNCT_1:def 3;
reconsider x = x as Nat by A8;
A9: dom (f *. o) = dom o by FOMODEL2:def 6;
n in dom (f *. o)

proof

assume not n in dom (f *. o) ; :: thesis: contradiction
then (f *. o) . n = {} by FUNCT_1:def 2;
hence contradiction by A7; :: thesis: verum

end;

then A10: (f *. o) . n = f * (o . n) by A9, FOMODEL2:def 6;
then A11: ( (f * (o . n)) . x = f . ((o . n) . x) & x in dom (o . n) ) by A8, FUNCT_1:11, FUNCT_1:12;
then ( 1 <= x & x <= len (o . n) ) by FINSEQ_3:25;
then ( w = f . (o _ (n,x)) & 1 <= len (o . n) ) by XXREAL_0:2, A5;
then z = f . (o _ (n,1)) by A5, A8, A11, A10;
hence z in {(f . (o _ (n,1)))} by TARSKI:def 1; :: thesis: verum

end;

hence ( rng ((f *. o) . n) = {(f . (o _ (n,1)))} & 1 in dom (o . n) ) by A6, FINSEQ_3:25, ZFMISC_1:33; :: thesis: verum