:: deftheorem Def7 defines Fredholm ORDEQ_01:def 7 :
for n being non zero Element of NAT
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
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'],(REAL-NS n))),(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) holds
( b₆ = Fredholm (G,a,b,y0) iff for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex f, g, Gf being continuous PartFunc of REAL,(REAL-NS n) 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)) ) ) );