defpred S1[ Nat, object , object ] means ex K being Lipschitzian LinearOperator of (diff_SP (($1 + 1),E,F)),(diff_SP (($1 + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP ($1,E,F)),(diff_SP ($1,E,G)) st
( $3 = K & In ($2,(R_NormSpace_of_BoundedLinearOperators ((diff_SP ($1,E,F)),(diff_SP ($1,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP ($1,E,F)) holds K . V = M * V ) );
let seq1, seq2 be Function; ( dom seq1 = NAT & seq1 . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( seq1 . (i + 1) = K & In ((seq1 . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) & dom seq2 = NAT & seq2 . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( seq2 . (i + 1) = K & In ((seq2 . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) implies seq1 = seq2 )
assume that
A21:
( dom seq1 = NAT & seq1 . 0 = L & ( for n being Nat holds S1[n,seq1 . n,seq1 . (n + 1)] ) )
and
A22:
( dom seq2 = NAT & seq2 . 0 = L & ( for n being Nat holds S1[n,seq2 . n,seq2 . (n + 1)] ) )
; seq1 = seq2
defpred S2[ Nat] means seq1 . $1 = seq2 . $1;
A23:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A24:
S2[
k]
;
S2[k + 1]
consider K1 being
Lipschitzian LinearOperator of
(diff_SP ((k + 1),E,F)),
(diff_SP ((k + 1),E,G)),
M1 being
Lipschitzian LinearOperator of
(diff_SP (k,E,F)),
(diff_SP (k,E,G)) such that A25:
(
seq1 . (k + 1) = K1 &
In (
(seq1 . k),
(R_NormSpace_of_BoundedLinearOperators ((diff_SP (k,E,F)),(diff_SP (k,E,G)))))
= M1 & ( for
V being
Lipschitzian LinearOperator of
E,
(diff_SP (k,E,F)) holds
K1 . V = M1 * V ) )
by A21;
consider K2 being
Lipschitzian LinearOperator of
(diff_SP ((k + 1),E,F)),
(diff_SP ((k + 1),E,G)),
M2 being
Lipschitzian LinearOperator of
(diff_SP (k,E,F)),
(diff_SP (k,E,G)) such that A26:
(
seq2 . (k + 1) = K2 &
In (
(seq2 . k),
(R_NormSpace_of_BoundedLinearOperators ((diff_SP (k,E,F)),(diff_SP (k,E,G)))))
= M2 & ( for
V being
Lipschitzian LinearOperator of
E,
(diff_SP (k,E,F)) holds
K2 . V = M2 * V ) )
by A22;
for
x being
Element of the
carrier of
(diff_SP ((k + 1),E,F)) holds
K1 . x = K2 . x
proof
let x be
Element of the
carrier of
(diff_SP ((k + 1),E,F));
K1 . x = K2 . x
diff_SP (
(k + 1),
E,
F)
= R_NormSpace_of_BoundedLinearOperators (
E,
(diff_SP (k,E,F)))
by NDIFF_6:10;
then reconsider V =
x as
Lipschitzian LinearOperator of
E,
(diff_SP (k,E,F)) by LOPBAN_1:def 9;
thus K1 . x =
M1 * V
by A25
.=
K2 . x
by A24, A25, A26
;
verum
end;
then
K1 = K2
;
hence
seq1 . (k + 1) = seq2 . (k + 1)
by A25, A26;
verum
end;
A27:
S2[ 0 ]
by A21, A22;
for n being Nat holds S2[n]
from NAT_1:sch 2(A27, A23);
then
for n being object st n in dom seq1 holds
seq1 . n = seq2 . n
by A21;
hence
seq1 = seq2
by A21, A22, FUNCT_1:2; verum