let f1, f2 be Function of V,INT.Ring; :: thesis: ( ( for v being Vector of V ex Lu being Linear_Combination of B st
( v = Sum Lu & f1 . v = Lu . u ) ) & ( for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
f1 . v = Lv . u ) & ( for v1, v2 being Vector of V holds f1 . (v1 + v2) = (f1 . v1) + (f1 . v2) ) & ( for v being Vector of V
for r being Element of INT.Ring holds f1 . (r * v) = r * (f1 . v) ) & ( for v being Vector of V ex Lu being Linear_Combination of B st
( v = Sum Lu & f2 . v = Lu . u ) ) & ( for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
f2 . v = Lv . u ) & ( for v1, v2 being Vector of V holds f2 . (v1 + v2) = (f2 . v1) + (f2 . v2) ) & ( for v being Vector of V
for r being Element of INT.Ring holds f2 . (r * v) = r * (f2 . v) ) implies f1 = f2 )
assume A1: ( ( for v being Vector of V ex Lu being Linear_Combination of B st
( v = Sum Lu & f1 . v = Lu . u ) ) & ( for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
f1 . v = Lv . u ) & ( for v1, v2 being Vector of V holds f1 . (v1 + v2) = (f1 . v1) + (f1 . v2) ) & ( for v being Vector of V
for r being Element of INT.Ring holds f1 . (r * v) = r * (f1 . v) ) ) ; :: thesis: ( ex v being Vector of V st
for Lu being Linear_Combination of B holds
( not v = Sum Lu or not f2 . v = Lu . u ) or ex v being Vector of V ex Lv being Linear_Combination of B st
( v = Sum Lv & not f2 . v = Lv . u ) or ex v1, v2 being Vector of V st not f2 . (v1 + v2) = (f2 . v1) + (f2 . v2) or ex v being Vector of V ex r being Element of INT.Ring st not f2 . (r * v) = r * (f2 . v) or f1 = f2 )
assume A2: ( ( for v being Vector of V ex Lu being Linear_Combination of B st
( v = Sum Lu & f2 . v = Lu . u ) ) & ( for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
f2 . v = Lv . u ) & ( for v1, v2 being Vector of V holds f2 . (v1 + v2) = (f2 . v1) + (f2 . v2) ) & ( for v being Vector of V
for r being Element of INT.Ring holds f2 . (r * v) = r * (f2 . v) ) ) ; :: thesis: f1 = f2
now :: thesis: for v being Vector of V holds f1 . v = f2 . v
let v be Vector of V; :: thesis: f1 . v = f2 . v
consider Lu being Linear_Combination of B such that
A3: ( v = Sum Lu & f1 . v = Lu . u ) by A1;
thus f1 . v = f2 . v by A2, A3; :: thesis: verum
end;
hence f1 = f2 by FUNCT_2:def 7; :: thesis: verum