theorem :: VECTSP11:22

for n being Nat
for K being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over K
for W being Subspace of V1
for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n