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) )
reconsider fg = f ^ g as FinSequence of NAT ;
assume A1: i in Seg (Sum f) ; :: thesis: min ((f ^ g),i) = min (f,i)
then A2: i <= Sum (f | (min (f,i))) by Def1;
Sum fg = (Sum f) + (Sum g) by RVSUM_1:75;
then Sum fg >= (Sum f) + 0 by XREAL_1:6;
then A3: Seg (Sum f) c= Seg (Sum fg) by FINSEQ_1:5;
min (f,i) in dom f by A1, Def1;
then A4: min (f,i) <= len f by FINSEQ_3:25;
then fg | (min (f,i)) = f | (min (f,i)) by FINSEQ_5:22;
then A5: min (fg,i) <= min (f,i) by A1, A3, A2, Def1;
then fg | (min (fg,i)) = f | (min (fg,i)) by A4, FINSEQ_5:22, XXREAL_0:2;
then i <= Sum (f | (min (fg,i))) by A1, A3, 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