let n be Nat; :: thesis: 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
let K be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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
let V1 be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over K; :: thesis: 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
let W be Subspace of V1; :: thesis: for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
let f be Function of V1,V1; :: thesis: for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
let fW be Function of W,W; :: thesis: ( fW = f | W implies (f |^ n) | W = fW |^ n )
assume A1: fW = f | W ; :: thesis: (f |^ n) | W = fW |^ n
defpred S₁[ Nat] means (f |^ $1) | W = fW |^ $1;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
A4: rng (fW |^ n) c= [#] W by RELAT_1:def 19;
thus (f |^ (n + 1)) | W = ((f |^ 1) * (f |^ n)) | W by Th20
.= (f |^ 1) * ((f |^ n) | W) by RELAT_1:83
.= (f |^ 1) * ((id W) * (fW |^ n)) by A3, A4, RELAT_1:53
.= ((f |^ 1) * (id W)) * (fW |^ n) by RELAT_1:36
.= (f * (id W)) * (fW |^ n) by Th19
.= fW * (fW |^ n) by A1, RELAT_1:65
.= (fW |^ 1) * (fW |^ n) by Th19
.= fW |^ (n + 1) by Th20 ; :: thesis: verum

end;

[#] W c= [#] V1 by VECTSP_4:def 2;
then A5: [#] W = ([#] V1) /\ ([#] W) by XBOOLE_1:28;
(f |^ 0) | W = (id V1) | W by Th18
.= (id V1) * (id W) by RELAT_1:65
.= id W by A5, FUNCT_1:22
.= fW |^ 0 by Th18 ;
then A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A2);
hence (f |^ n) | W = fW |^ n ; :: thesis: verum