consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that
A2: ( f = g & x = y & g is_partial_differentiable_in y,i ) by A1, Def13;
A3: <*1*> is Element of REAL 1 by FINSEQ_2:118;
( the carrier of (REAL-NS 1) = REAL 1 & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then partdiff g,y,i is Function of (REAL 1),(REAL n) by LOPBAN_1:def 10;
then (partdiff g,y,i) . <*1*> is Element of REAL n by A3, FUNCT_2:7;
hence ( ex b₁ being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b₁ = (partdiff g,y,i) . <*1*> ) & ( for b₁, b₂ being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b₁ = (partdiff g,y,i) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b₂ = (partdiff g,y,i) . <*1*> ) holds
b₁ = b₂ ) ) by A2; :: thesis: verum