let s be 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] )
let p be 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] )
let v be Element of dom p; ( (p . v) `2 = 1 implies 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] ) )
A1:
v is correct
by Def12;
assume A2:
(p . v) `2 = 1
; 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] )
then A3:
ex T being FinSequence of s ex x, y being type of s st
( (p . v) `1 = [T,(x /" y)] & (p . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] )
by A1, Def4;
branchdeg v = 1
by A1, A2, Def4;
then
v ^ <*0*> in dom p
by Th1;
hence
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] )
by A3; verum