let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L
for b being bag of n
for i being Nat st i <> 0 holds
eval ((i (#) b),x) = (power L) . ((eval (b,x)),i)
let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x being Function of n,L
for b being bag of n
for i being Nat st i <> 0 holds
eval ((i (#) b),x) = (power L) . ((eval (b,x)),i)
let x be Function of n,L; :: thesis: for b being bag of n
for i being Nat st i <> 0 holds
eval ((i (#) b),x) = (power L) . ((eval (b,x)),i)
let b be bag of n; :: thesis: for i being Nat st i <> 0 holds
eval ((i (#) b),x) = (power L) . ((eval (b,x)),i)
defpred S₁[ Nat] means ( $1 <> 0 implies eval (($1 (#) b),x) = (power L) . ((eval (b,x)),$1) );
A1: S₁[ 0 ] ;
A2: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A3: S₁[j] ; :: thesis: S₁[j + 1]
assume j + 1 <> 0 ; :: thesis: eval (((j + 1) (#) b),x) = (power L) . ((eval (b,x)),(j + 1))

per cases ( j = 0 or j <> 0 ) ;

suppose A4: j = 0 ; :: thesis: eval (((j + 1) (#) b),x) = (power L) . ((eval (b,x)),(j + 1))

hence eval (((j + 1) (#) b),x) = eval (b,x) by RFUNCT_1:21
.= (power L) . ((eval (b,x)),(j + 1)) by A4, GROUP_1:50 ;
:: thesis: verum

end;

suppose A5: j <> 0 ; :: thesis: eval (((j + 1) (#) b),x) = (power L) . ((eval (b,x)),(j + 1))

thus eval (((j + 1) (#) b),x) = eval (((j (#) b) + (1 (#) b)),x) by TOPREALC:2
.= (eval ((j (#) b),x)) * (eval ((1 (#) b),x)) by POLYNOM2:16
.= ((power L) . ((eval (b,x)),j)) * (eval (b,x)) by A5, A3, RFUNCT_1:21
.= (power L) . ((eval (b,x)),(j + 1)) by GROUP_1:def 7 ; :: thesis: verum

end;

end;

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A1, A2);
hence for i being Nat st i <> 0 holds
eval ((i (#) b),x) = (power L) . ((eval (b,x)),i) ; :: thesis: verum