let i be Nat; 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 ; ( 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)
; 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; verum