:: On Cosets in Segre's Product of Partial Linear Spaces :: by Adam Naumowicz :: :: Received August 14, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users
A1:
( F1() = F4() . 1 & F2() = F4() .(len F4()) )
and A2:
for i being Element of NAT for d1, d2 being set st 1 <= i & i <len F4() & d1 = F4() . i & d2 = F4() .(i + 1) holds P1[d1,d2]