let f be FinSequence of COMPLEX ; :: thesis: XProduct (FS2XFS f) = Product f
reconsider g = FS2XFS f as XFinSequence of COMPLEX ;
XProduct g = Product (XFS2FS g) by XPF
.= Product f ;
hence XProduct (FS2XFS f) = Product f ; :: thesis: verum