:: deftheorem Def8 defines Fredholm ORDEQ_02:def 1 :
for X being RealBanachSpace
for y0 being VECTOR of X
for G being Function of X,X
for a, b being Real st a <= b & G is_continuous_on dom G holds
for b₆ being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds
( b₆ = Fredholm (G,a,b,y0) iff for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X st
( x = f & b₆ . x = g & dom f = ['a,b'] & dom g = ['a,b'] & Gf = G * f & ( for t being Real st t in ['a,b'] holds
g /. t = y0 + (integral (Gf,a,t)) ) ) );