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

let x be set ; :: thesis: ( x in the carrier of V1 implies F1 . x = F2 . x )
assume A4: x in the carrier of V1 ; :: thesis: F1 . x = F2 . x
reconsider v = x as Vector of V1 by A4;
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:18; :: thesis: verum