let n be Nat; :: thesis: for f being real-valued finite-support Function st f <= n holds
for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F <= n
let f be real-valued finite-support Function; :: thesis: ( f <= n implies for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F <= n )
assume A1: f <= n ; :: thesis: for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F <= n
set b = (EmptyBag SetPrimes) +* f;
set C = canFS (support ((EmptyBag SetPrimes) +* f));
let F be real-valued FinSequence; :: thesis: ( F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) implies F <= n )
assume A2: F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) ; :: thesis: F <= n
let x be object ; :: according to NUMBER08:def 4 :: thesis: ( x in dom F implies F . x <= n )
assume A3: x in dom F ; :: thesis: F . x <= n
set y = (canFS (support ((EmptyBag SetPrimes) +* f))) . x;
A4: F . x = ((EmptyBag SetPrimes) +* f) . ((canFS (support ((EmptyBag SetPrimes) +* f))) . x) by A2, A3, FUNCT_1:12;

per cases ( (canFS (support ((EmptyBag SetPrimes) +* f))) . x in dom f or not (canFS (support ((EmptyBag SetPrimes) +* f))) . x in dom f ) ;

suppose A5: (canFS (support ((EmptyBag SetPrimes) +* f))) . x in dom f ; :: thesis: F . x <= n

then ((EmptyBag SetPrimes) +* f) . ((canFS (support ((EmptyBag SetPrimes) +* f))) . x) = f . ((canFS (support ((EmptyBag SetPrimes) +* f))) . x) by FUNCT_4:13;
hence F . x <= n by A1, A4, A5; :: thesis: verum

end;

suppose not (canFS (support ((EmptyBag SetPrimes) +* f))) . x in dom f ; :: thesis: F . x <= n

then ((EmptyBag SetPrimes) +* f) . ((canFS (support ((EmptyBag SetPrimes) +* f))) . x) = (EmptyBag SetPrimes) . ((canFS (support ((EmptyBag SetPrimes) +* f))) . x) by FUNCT_4:11;
hence F . x <= n by A2, A3, FUNCT_1:12; :: thesis: verum

end;

end;