let n be Nat; :: thesis: for K being Field
for a being Element of K holds Product (n |-> a) = (power K) . (a,n)
let K be Field; :: thesis: for a being Element of K holds Product (n |-> a) = (power K) . (a,n)
let a be Element of K; :: thesis: Product (n |-> a) = (power K) . (a,n)
defpred S₁[ Nat] means Product ($1 |-> a) = (power K) . (a,$1);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
thus Product ((k + 1) |-> a) = (Product (k |-> a)) * (Product (1 |-> a)) by FVSUM_1:83
.= (Product (k |-> a)) * (Product <*a*>) by FINSEQ_2:59
.= ((power K) . (a,k)) * a by A2, GROUP_4:9
.= (power K) . (a,(k + 1)) by GROUP_1:def 7 ; :: thesis: verum

end;

0 |-> a = <*> the carrier of K ;
then Product (0 |-> a) = 1_ K by GROUP_4:8
.= (power K) . (a,0) by GROUP_1:def 7 ;
then A3: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
hence Product (n |-> a) = (power K) . (a,n) ; :: thesis: verum