let s be non empty typealg ; :: thesis: 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] )
let z be type of s; :: thesis: 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] )
let p be Proof of s; :: thesis: 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] )
let v be Element of dom p; :: thesis: ( (p . v) `2 = 5 implies 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] ) )
A1: v is correct by Def12;
assume A2: (p . v) `2 = 5 ; :: thesis: 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] )
then A3: ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st
( (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) 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 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] ) by A3; :: thesis: verum