let f be XFinSequence of COMPLEX ; :: thesis: for g being FinSequence of COMPLEX holds
( XProduct (f ^ g) = (XProduct f) * (Product g) & Product (g ^ f) = (Product g) * (XProduct f) )
let g be FinSequence of COMPLEX ; :: thesis: ( XProduct (f ^ g) = (XProduct f) * (Product g) & Product (g ^ f) = (Product g) * (XProduct f) )
A1: XProduct (f ^ g) = Product (XFS2FS (f ^ g)) by XPF
.= Product ((XFS2FS f) ^ g) by SSX
.= (Product (XFS2FS f)) * (Product g) by FAF
.= (XProduct f) * (Product g) by XPF ;
Product (g ^ f) = Product (g ^ (FS2XFS (XFS2FS f)))
.= Product (g ^ (XFS2FS f)) by FXF
.= (Product g) * (Product (XFS2FS f)) by FAF
.= (Product g) * (XProduct f) by XPF ;
hence ( XProduct (f ^ g) = (XProduct f) * (Product g) & Product (g ^ f) = (Product g) * (XProduct f) ) by A1; :: thesis: verum