theorem :: PRELAMB:7

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