thus ( (p . {}) `2 = 7 implies ex r being Nat ex T, X, Y being FinSequence of s ex y, z being type of s st
( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) ) :: thesis: ( not (p . {}) `2 = 7 implies ex b₁ being Nat st b₁ = 0 )

proof

A1: {} ^ <*0*> = <*0*> by FINSEQ_1:47;
A2: {} ^ <*1*> = <*1*> by FINSEQ_1:47;
reconsider v = {} as Element of dom p by TREES_1:47;
assume (p . {}) `2 = 7 ; :: thesis: ex r being Nat ex T, X, Y being FinSequence of s ex y, z being type of s st
( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) )
then consider w, u being Element of dom p, T, X, Y being FinSequence of s, y, z being type of s such that
A3: w = v ^ <*0*> and
A4: u = v ^ <*1*> and
A5: (p . v) `1 = [((X ^ T) ^ Y),z] and
A6: (p . w) `1 = [T,y] and
A7: (p . u) `1 = [((X ^ <*y*>) ^ Y),z] by Th10;
reconsider a = Sum ((size_w.r.t. s) * ((X ^ T) ^ Y)) as Nat by Lm3;
take (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a ; :: thesis: ex T, X, Y being FinSequence of s ex y, z being type of s st
( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) )
thus ex T, X, Y being FinSequence of s ex y, z being type of s st
( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) by A1, A2, A3, A4, A5, A6, A7; :: thesis: verum

end;

thus ( not (p . {}) `2 = 7 implies ex b₁ being Nat st b₁ = 0 ) ; :: thesis: verum