let i, j be Nat; :: thesis: for S being 1-sorted
for F being Function of S,S holds F |^ (i + j) = (F |^ i) * (F |^ j)
let S be 1-sorted ; :: thesis: for F being Function of S,S holds F |^ (i + j) = (F |^ i) * (F |^ j)
let F be Function of S,S; :: thesis: F |^ (i + j) = (F |^ i) * (F |^ j)
set G = GFuncs the carrier of S;
reconsider Fg = F as Element of (GFuncs the carrier of S) by MONOID_0:82;
reconsider G = GFuncs the carrier of S as non empty unital associative multMagma ;
reconsider F' = F as Element of G by MONOID_0:82;
Product ((i + j) |-> F') = Product ((i |-> F') ^ (j |-> F')) by FINSEQ_2:143
.= (Product (i |-> F')) * (Product (j |-> F')) by GROUP_4:8
.= (Product (i |-> Fg)) (*) (Product (j |-> Fg)) by MONOID_0:79
.= (F |^ i) (*) (Product (j |-> Fg)) by Def4
.= (F |^ i) (*) (F |^ j) by Def4 ;
hence F |^ (i + j) = (F |^ i) * (F |^ j) by Def4; :: thesis: verum