let F1, F2 be Function of V,R^1; :: thesis: ( ( for v being VECTOR of V holds F1 . v = (v |-- A) . x ) & ( for v being VECTOR of V holds F2 . v = (v |-- A) . x ) implies F1 = F2 )
assume that
A3: for v being Element of V holds F1 . v = (v |-- A) . x and
A4: for v being Element of V holds F2 . v = (v |-- A) . x ; :: thesis: F1 = F2

now :: thesis: for v being object st v in the carrier of V holds
F1 . v = F2 . v

let v be object ; :: thesis: ( v in the carrier of V implies F1 . v = F2 . v )
assume A5: v in the carrier of V ; :: thesis: F1 . v = F2 . v
hence F1 . v = (v |-- A) . x by A3
.= F2 . v by A4, A5 ;
:: thesis: verum

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum