let r1, r2 be Nat; :: thesis: ( ( (p . {}) `2 = 7 & 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] & r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) & 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] & r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) implies r1 = r2 ) & ( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 ) )
thus ( (p . {}) `2 = 7 & 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] & r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) & 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] & r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) implies r1 = r2 ) :: thesis: ( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 )

proof

assume (p . {}) `2 = 7 ; :: thesis: ( for T, X, Y being FinSequence of s
for y, z being type of s holds
( not (p . {}) `1 = [((X ^ T) ^ Y),z] or not (p . <*0*>) `1 = [T,y] or not (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] or not r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) or for T, X, Y being FinSequence of s
for y, z being type of s holds
( not (p . {}) `1 = [((X ^ T) ^ Y),z] or not (p . <*0*>) `1 = [T,y] or not (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] or not r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) or r1 = r2 )
given T, X, Y being FinSequence of s, y, z being type of s such that A8: (p . {}) `1 = [((X ^ T) ^ Y),z] and
A9: (p . <*0*>) `1 = [T,y] and
(p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] and
A10: r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ; :: thesis: ( for T, X, Y being FinSequence of s
for y, z being type of s holds
( not (p . {}) `1 = [((X ^ T) ^ Y),z] or not (p . <*0*>) `1 = [T,y] or not (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] or not r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) or r1 = r2 )
given T9, X9, Y9 being FinSequence of s, y9, z9 being type of s such that A11: (p . {}) `1 = [((X9 ^ T9) ^ Y9),z9] and
A12: (p . <*0*>) `1 = [T9,y9] and
(p . <*1*>) `1 = [((X9 ^ <*y9*>) ^ Y9),z9] and
A13: r2 = (((size_w.r.t. s) . y9) + ((size_w.r.t. s) . z9)) + (Sum ((size_w.r.t. s) * ((X9 ^ T9) ^ Y9))) ; :: thesis: r1 = r2
A14: (X ^ T) ^ Y = [((X ^ T) ^ Y),z] `1
.= [((X9 ^ T9) ^ Y9),z9] `1 by A8, A11
.= (X9 ^ T9) ^ Y9 ;
A15: y = [T,y] `2
.= [T9,y9] `2 by A9, A12
.= y9 ;
z = [((X ^ T) ^ Y),z] `2
.= [((X9 ^ T9) ^ Y9),z9] `2 by A8, A11
.= z9 ;
hence r1 = r2 by A10, A13, A14, A15; :: thesis: verum

end;

thus ( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 ) ; :: thesis: verum