:: A Theory of Sequential Files :: by Hirofumi Fukura and Yatsuka Nakamura :: :: Received August 12, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users
for D being non emptyset for p, q, r, s being FinSequence of D holds ( ((p ^ q)^ r)^ s =(p ^(q ^ r))^ s & ((p ^ q)^ r)^ s =(p ^ q)^(r ^ s) & (p ^(q ^ r))^ s =(p ^ q)^(r ^ s) )