let X be Ordinal; :: thesis: for S being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of X,S
for k being Nat holds vars (p `^ k) c= vars p
let S be non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of X,S
for k being Nat holds vars (p `^ k) c= vars p
let p be Polynomial of X,S; :: thesis: for k being Nat holds vars (p `^ k) c= vars p
defpred S<sub>1</sub>[ Nat] means vars (p `^ $1) c= vars p;
p `^ 0 = 1_ (X,S) by Th28;
then vars (p `^ 0) = {} by Th38;
then A1: S₁[ 0 ] by XBOOLE_1:2;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then A3: (vars (p `^ k)) \/ (vars p) c= (vars p) \/ (vars p) by XBOOLE_1:9;
p `^ (k + 1) = (p `^ k) *' p by Th29;
then vars (p `^ (k + 1)) c= (vars (p `^ k)) \/ (vars p) by Th43;
hence S₁[k + 1] by A3, XBOOLE_1:1; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence for k being Nat holds vars (p `^ k) c= vars p ; :: thesis: verum