let i be Nat; :: thesis: for f being FinSequence
for o1, o2 being valued_reorganization of f st rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
rng (o1 . i) c= rng (o2 . i)
let f be FinSequence; :: thesis: for o1, o2 being valued_reorganization of f st rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
rng (o1 . i) c= rng (o2 . i)
let o1, o2 be valued_reorganization of f; :: thesis: ( rng ((f *. o1) . i) = rng ((f *. o2) . i) implies rng (o1 . i) c= rng (o2 . i) )
assume A1: rng ((f *. o1) . i) = rng ((f *. o2) . i) ; :: thesis: rng (o1 . i) c= rng (o2 . i)
len ((f *. o1) . i) = len (o1 . i) by CARD_1:def 7;
then A2: dom (o1 . i) = dom ((f *. o1) . i) by FINSEQ_3:29;
A3: len ((f *. o2) . i) = len (o2 . i) by CARD_1:def 7;
A4: ( Values o1 = dom f & Values o2 = dom f ) by Def7;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o1 . i) or y in rng (o2 . i) )
assume y in rng (o1 . i) ; :: thesis: y in rng (o2 . i)
then consider x being object such that
A5: ( x in dom (o1 . i) & (o1 . i) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A5;
((f *. o1) . i) . x in rng ((f *. o2) . i) by A2, A5, FUNCT_1:def 3, A1;
then consider u being object such that
A6: ( u in dom ((f *. o2) . i) & ((f *. o2) . i) . u = ((f *. o1) . i) . x ) by FUNCT_1:def 3;
A7: (f *. o1) _ (i,x) = f . (o1 _ (i,x)) by Th42;
A8: (f *. o2) _ (i,u) = f . (o2 _ (i,u)) by Th42;
i in dom o1

proof

assume not i in dom o1 ; :: thesis: contradiction
then o1 . i = {} by FUNCT_1:def 2;
hence contradiction by A5; :: thesis: verum

end;

then consider j, w being object such that
A9: ( j in dom o2 & w in dom (o2 . j) & (o2 . j) . w = y ) by Th1, A5, A4;
A10: u in dom (o2 . i) by A6, A3, FINSEQ_3:29;
f . (o2 _ (i,u)) = f . (o2 _ (j,w)) by A5, A9, A6, A7, A8;
then j = i by Def9, A10, A9;
hence y in rng (o2 . i) by A9, FUNCT_1:def 3; :: thesis: verum