let f be non empty complex-valued XFinSequence; :: thesis: XProduct (f | 1) = f . 0
1 <= len f by NAT_1:14;
then B2: len (f | 1) = 1 by AFINSQ_1:54;
then 0 in Segm (len (f | 1)) by NAT_1:44;
then ( 0 in dom f & 0 in 1 ) by RELAT_1:57;
then B3: 0 in (dom f) /\ 1 by XBOOLE_0:def 4;
XProduct (f | 1) = XProduct <%((f | 1) . 0)%> by B2, AFINSQ_1:34
.= f . 0 by B3, FUNCT_1:48 ;
hence XProduct (f | 1) = f . 0 ; :: thesis: verum