let m be non zero 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 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 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 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 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 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