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 VectSp-like Abelian add-associative right_zeroed VectSpStr of 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 VectSp-like Abelian add-associative right_zeroed VectSpStr of 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 VectSp-like Abelian add-associative right_zeroed VectSpStr of 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: S₁[ 0 ]

proof

[#] W c= [#] V1 by VECTSP_4:def 2;
then A3: [#] W = ([#] V1) /\ ([#] W) by XBOOLE_1:28;
thus (f |^ 0 ) | W = (id V1) | W by Th18
.= (id V1) * (id W) by RELAT_1:94
.= id W by A3, FUNCT_1:43
.= fW |^ 0 by Th18 ; :: thesis: verum

end;

A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: 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:112
.= (f |^ 1) * ((id W) * (fW |^ n)) by A5, A6, RELAT_1:79
.= ((f |^ 1) * (id W)) * (fW |^ n) by RELAT_1:55
.= (f * (id W)) * (fW |^ n) by Th19
.= fW * (fW |^ n) by A1, RELAT_1:94
.= (fW |^ 1) * (fW |^ n) by Th19
.= fW |^ (n + 1) by Th20 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A4);
hence (f |^ n) | W = fW |^ n ; :: thesis: verum