let F1, F2 be Function of V1,V2; :: thesis: ( ( for v being Vector of V1 holds F1 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) & ( for v being Vector of V1 holds F2 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) implies F1 = F2 )
assume that
A2: for v being Vector of V1 holds F1 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) and
A3: for v being Vector of V1 holds F2 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ; :: thesis: F1 = F2

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

let x be object ; :: thesis: ( x in the carrier of V1 implies F1 . x = F2 . x )
assume x in the carrier of V1 ; :: thesis: F1 . x = F2 . x
then reconsider v = x as Vector of V1 ;
thus F1 . x = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) by A2
.= F2 . x by A3 ; :: thesis: verum

end;

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