let m be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for g being PartFunc of REAL ,REAL
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) holds
diff g,xi = partdiff f,y,i
let f be PartFunc of (REAL m),REAL ; :: thesis: for g being PartFunc of REAL ,REAL
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) holds
diff g,xi = partdiff f,y,i
let g be PartFunc of REAL ,REAL ; :: thesis: for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) holds
diff g,xi = partdiff f,y,i
let x, y be Element of REAL m; :: thesis: for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) holds
diff g,xi = partdiff f,y,i
let i be Element of NAT ; :: thesis: for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) holds
diff g,xi = partdiff f,y,i
let xi be Real; :: thesis: ( 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) implies diff g,xi = partdiff f,y,i )
assume A1: ( 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) ) ; :: thesis: diff g,xi = partdiff f,y,i
then ( reproj i,x = reproj i,y & (proj i,m) . y = xi ) by Th39, Th40;
hence partdiff f,y,i = diff g,xi by A1; :: thesis: verum