theorem :: PRELAMB:4

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