theorem :: PRELAMB:8

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