let s be non empty typealg ; :: thesis: 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 the carrier 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] )
let p be Proof of s; :: thesis: 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 the carrier 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] )
let v be Element of dom p; :: thesis: ( (p . v) `2 = 4 implies ex w, u being Element of dom p ex T, X, Y being FinSequence of the carrier 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] ) )
A1: v is correct by Def13;
assume A2: (p . v) `2 = 4 ; :: thesis: ex w, u being Element of dom p ex T, X, Y being FinSequence of the carrier 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] )
then A3: ex T, X, Y being FinSequence of the carrier of s ex x, y, z being type of s st
( (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . (v ^ <*0 *>)) `1 = [T,y] & (p . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) by A1, Def5;
branchdeg v = 2 by A1, A2, Def5;
then ( v ^ <*0 *> in dom p & v ^ <*1*> in dom p ) by Th2;
hence ex w, u being Element of dom p ex T, X, Y being FinSequence of the carrier 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] ) by A3; :: thesis: verum