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

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

hence
F1 = F2
by FUNCT_2:12; :: thesis: verumF1 . 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;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