let K be Field; 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; 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; 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; 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; 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; ( F = f | W1 implies F is linear-transformation of W1,W2 )
assume A1:
F = f | W1
; F is linear-transformation of W1,W2
now for w1, w2 being Vector of W1 holds F . (w1 + w2) = (F . w1) + (F . w2)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
; verum