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

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, MOD_2:def 5
.= (F . w1) + (F . w2) by A1, VECTSP_4:21 ; :: thesis: verum

end;

now

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 5
.= a * (F . w) by A1, VECTSP_4:22 ; :: thesis: verum

end;

hence F is linear-transformation of W1,W2 by A2, MOD_2:def 5; :: thesis: verum