theorem Th10: :: PRELAMB:10

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