let K be Field; :: thesis: for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let V1, V2 be VectSp of K; :: thesis: for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let f be linear-transformation of V1,V2; :: thesis: for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let W1 be Subspace of V1; :: thesis: for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let W2 be Subspace of V2; :: thesis: for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let F be Function of W1,W2; :: thesis: ( F = f | W1 implies F is linear-transformation of W1,W2 )
assume A1: F = f | W1 ; :: thesis: F is linear-transformation of W1,W2

A2: now :: thesis: for a being Scalar of K
for w being Vector of W1 holds F . (a * w) = a * (F . w)

let a be Scalar of K; :: thesis: for w being Vector of W1 holds F . (a * w) = a * (F . w)
let w be Vector of W1; :: thesis: F . (a * w) = a * (F . w)
thus F . (a * w) = a * ((f | W1) . w) by A1, MOD_2:def 2
.= a * (F . w) by A1, VECTSP_4:14 ; :: thesis: verum

end;

now :: thesis: for w1, w2 being Vector of W1 holds F . (w1 + w2) = (F . w1) + (F . w2)

let w1, w2 be Vector of W1; :: thesis: F . (w1 + w2) = (F . w1) + (F . w2)
thus F . (w1 + w2) = ((f | W1) . w1) + ((f | W1) . w2) by A1, VECTSP_1:def 20
.= (F . w1) + (F . w2) by A1, VECTSP_4:13 ; :: thesis: verum

end;

then ( F is additive & F is homogeneous ) by A2, MOD_2:def 2, VECTSP_1:def 20;
hence F is linear-transformation of W1,W2 ; :: thesis: verum