let E, F be RealNormSpace; :: thesis: for Z being non empty Subset of E
for L1 being PartFunc of E,F
for L0 being Point of F st Z is open & L1 = Z --> L0 holds
for i being Nat holds
( ex P being Point of (diff_SP (i,E,F)) st diff (L1,i,Z) = Z --> P & diff (L1,i,Z) is_differentiable_on Z & (diff (L1,i,Z)) `| Z is_continuous_on Z )
let Z be non empty Subset of E; :: thesis: for L1 being PartFunc of E,F
for L0 being Point of F st Z is open & L1 = Z --> L0 holds
for i being Nat holds
( ex P being Point of (diff_SP (i,E,F)) st diff (L1,i,Z) = Z --> P & diff (L1,i,Z) is_differentiable_on Z & (diff (L1,i,Z)) `| Z is_continuous_on Z )
let L1 be PartFunc of E,F; :: thesis: for L0 being Point of F st Z is open & L1 = Z --> L0 holds
for i being Nat holds
( ex P being Point of (diff_SP (i,E,F)) st diff (L1,i,Z) = Z --> P & diff (L1,i,Z) is_differentiable_on Z & (diff (L1,i,Z)) `| Z is_continuous_on Z )
let L0 be Point of F; :: thesis: ( Z is open & L1 = Z --> L0 implies for i being Nat holds
( ex P being Point of (diff_SP (i,E,F)) st diff (L1,i,Z) = Z --> P & diff (L1,i,Z) is_differentiable_on Z & (diff (L1,i,Z)) `| Z is_continuous_on Z ) )
assume A1: ( Z is open & L1 = Z --> L0 ) ; :: thesis: for i being Nat holds
( ex P being Point of (diff_SP (i,E,F)) st diff (L1,i,Z) = Z --> P & diff (L1,i,Z) is_differentiable_on Z & (diff (L1,i,Z)) `| Z is_continuous_on Z )
defpred S<sub>1</sub>[ Nat] means ( ex P being Point of (diff_SP ($1,E,F)) st diff (L1,$1,Z) = Z --> P & diff (L1,$1,Z) is_differentiable_on Z & (diff (L1,$1,Z)) `| Z is_continuous_on Z );
A2: S₁[ 0 ]

proof

A3: diff_SP (0,E,F) = F by NDIFF_6:7;
A4: diff (L1,0,Z) = L1 | Z by NDIFF_6:11
.= L1 by A1 ;
thus ex P being Point of (diff_SP (0,E,F)) st diff (L1,0,Z) = Z --> P by A1, A3, A4; :: thesis: ( diff (L1,0,Z) is_differentiable_on Z & (diff (L1,0,Z)) `| Z is_continuous_on Z )
thus diff (L1,0,Z) is_differentiable_on Z by A1, A3, A4, Th48; :: thesis: (diff (L1,0,Z)) `| Z is_continuous_on Z
thus (diff (L1,0,Z)) `| Z is_continuous_on Z by A1, A3, A4, Th48; :: thesis: verum

end;

A5: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
then consider P being Point of (diff_SP (i,E,F)) such that
A6: diff (L1,i,Z) = Z --> P ;
A7: diff_SP ((i + 1),E,F) = R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (i,E,F))) by NDIFF_6:10;
A8: diff (L1,(i + 1),Z) = (diff (L1,i,Z)) `| Z by NDIFF_6:13
.= Z --> (0. (diff_SP ((i + 1),E,F))) by A1, A6, A7, Th48 ;
hence ex P being Point of (diff_SP ((i + 1),E,F)) st diff (L1,(i + 1),Z) = Z --> P ; :: thesis: ( diff (L1,(i + 1),Z) is_differentiable_on Z & (diff (L1,(i + 1),Z)) `| Z is_continuous_on Z )
thus diff (L1,(i + 1),Z) is_differentiable_on Z by A1, A8, Th48; :: thesis: (diff (L1,(i + 1),Z)) `| Z is_continuous_on Z
thus (diff (L1,(i + 1),Z)) `| Z is_continuous_on Z by A1, A8, Th48; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A5);
hence for i being Nat holds
( ex P being Point of (diff_SP (i,E,F)) st diff (L1,i,Z) = Z --> P & diff (L1,i,Z) is_differentiable_on Z & (diff (L1,i,Z)) `| Z is_continuous_on Z ) ; :: thesis: verum