let v1, v2 be RealNormSpace; :: thesis: ( ex f being Function st
( dom f = NAT & v1 = f . (len X) & f . 0 = Y & ( for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) ) & ex f being Function st
( dom f = NAT & v2 = f . (len X) & f . 0 = Y & ( for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) ) implies v1 = v2 )
given f1 being Function such that A44: ( dom f1 = NAT & v1 = f1 . (len X) ) and
A45: f1 . 0 = Y and
A46: for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f1 . i & i + 1 = j & f1 . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ; :: thesis: ( for f being Function holds
( not dom f = NAT or not v2 = f . (len X) or not f . 0 = Y or ex i being Nat st
( i < len X & ( for fi being RealNormSpace
for j being Element of dom X holds
( not fi = f . i or not i + 1 = j or not f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) ) ) or v1 = v2 )
given f2 being Function such that A47: ( dom f2 = NAT & v2 = f2 . (len X) ) and
A48: f2 . 0 = Y and
A49: for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f2 . i & i + 1 = j & f2 . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ; :: thesis: v1 = v2
defpred S₁[ Nat] means ( $1 <= len X implies f1 . $1 = f2 . $1 );

now :: thesis: for j being Nat st ( j <= len X implies f1 . j = f2 . j ) & j + 1 <= len X holds
f1 . (j + 1) = f2 . (j + 1)

let j be Nat; :: thesis: ( ( j <= len X implies f1 . j = f2 . j ) & j + 1 <= len X implies f1 . (j + 1) = f2 . (j + 1) )
assume A50: ( j <= len X implies f1 . j = f2 . j ) ; :: thesis: ( j + 1 <= len X implies f1 . (j + 1) = f2 . (j + 1) )
assume A51: j + 1 <= len X ; :: thesis: f1 . (j + 1) = f2 . (j + 1)
A52: ex fi being RealNormSpace ex j1 being Element of dom X st
( fi = f1 . j & j + 1 = j1 & f1 . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j1),fi) ) by A46, A51, NAT_1:13;
ex fi being RealNormSpace ex j1 being Element of dom X st
( fi = f2 . j & j + 1 = j1 & f2 . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j1),fi) ) by A49, A51, NAT_1:13;
hence f1 . (j + 1) = f2 . (j + 1) by A50, A51, A52, NAT_1:13; :: thesis: verum

end;

then A53: for j being Nat st S₁[j] holds
S₁[j + 1] ;
A54: S₁[ 0 ] by A45, A48;
for j being Nat holds S₁[j] from NAT_1:sch 2(A54, A53);
hence v1 = v2 by A44, A47; :: thesis: verum