let G be non-trivial RealNormSpace-Sequence; :: thesis: for F being non trivial RealNormSpace
for i being Element of dom G
for x being Point of (product G)
for xi being Point of (G . i)
for f being PartFunc of (product G),F
for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,x,i)
let F be non trivial RealNormSpace; :: thesis: for i being Element of dom G
for x being Point of (product G)
for xi being Point of (G . i)
for f being PartFunc of (product G),F
for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,x,i)
let i be Element of dom G; :: thesis: for x being Point of (product G)
for xi being Point of (G . i)
for f being PartFunc of (product G),F
for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,x,i)
let x be Point of (product G); :: thesis: for xi being Point of (G . i)
for f being PartFunc of (product G),F
for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,x,i)
let xi be Point of (G . i); :: thesis: for f being PartFunc of (product G),F
for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,x,i)
let f be PartFunc of (product G),F; :: thesis: for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,x,i)
let g be PartFunc of (G . i),F; :: thesis: ( (proj i) . x = xi & g = f * (reproj (i,x)) implies diff (g,xi) = partdiff (f,x,i) )
i = modetrans (G,i) by Defmode;
hence ( (proj i) . x = xi & g = f * (reproj (i,x)) implies diff (g,xi) = partdiff (f,x,i) ) ; :: thesis: verum