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