theorem :: PRELAMB:9

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 6 holds
ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st
( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] )