let f, g be ext-real-valued FinSequence; :: thesis: ( f ^ g is with_values_greater_or_equal_one implies ( f is with_values_greater_or_equal_one & g is with_values_greater_or_equal_one ) )
( rng f c= rng (f ^ g) & rng g c= rng (f ^ g) ) by FINSEQ_1:29, FINSEQ_1:30;
hence ( f ^ g is with_values_greater_or_equal_one implies ( f is with_values_greater_or_equal_one & g is with_values_greater_or_equal_one ) ) ; :: thesis: verum