let i be Nat; :: thesis: for f, g being FinSequence of NAT st i in Seg (Sum f) holds
min (f ^ g),i = min f,i
let f, g be FinSequence of NAT ; :: thesis: ( i in Seg (Sum f) implies min (f ^ g),i = min f,i )
assume A1: i in Seg (Sum f) ; :: thesis: min (f ^ g),i = min f,i
reconsider fg = f ^ g as FinSequence of NAT ;
Sum fg = (Sum f) + (Sum g) by RVSUM_1:105;
then Sum fg >= (Sum f) + 0 by XREAL_1:8;
then A2: Seg (Sum f) c= Seg (Sum fg) by FINSEQ_1:7;
min f,i in dom f by A1, Def1;
then A3: min f,i <= len f by FINSEQ_3:27;
then A4: fg | (min f,i) = f | (min f,i) by FINSEQ_5:25;
i <= Sum (f | (min f,i)) by A1, Def1;
then A5: min fg,i <= min f,i by A1, A2, A4, Def1;
then fg | (min fg,i) = f | (min fg,i) by A3, FINSEQ_5:25, XXREAL_0:2;
then i <= Sum (f | (min fg,i)) by A1, A2, Def1;
then min f,i <= min fg,i by A1, Def1;
hence min (f ^ g),i = min f,i by A5, XXREAL_0:1; :: thesis: verum