let r1, r2 be Nat; ( ( (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 )
( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 )proof
assume
(p . {}) `2 = 7
;
( 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)))
;
( 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)))
;
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;
verum
end;
thus
( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 )
; verum