let X, Y, W be RealNormSpace; :: thesis: for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) & partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) )
let z be Point of [:X,Y:]; :: thesis: for f being PartFunc of [:X,Y:],W holds
( partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) & partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) )
let f be PartFunc of [:X,Y:],W; :: thesis: ( partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) & partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) )
reconsider g = f * ((IsoCPNrSP (X,Y)) ") as PartFunc of (product <*X,Y*>),W ;
reconsider w = (IsoCPNrSP (X,Y)) . z as Element of (product <*X,Y*>) ;
D1: dom <*X,Y*> = Seg (len <*X,Y*>) by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44 ;
then 1 in dom <*X,Y*> ;
then AS1: In (1,(dom <*X,Y*>)) = 1 by SUBSET_1:def 8;
2 in dom <*X,Y*> by D1;
then AS2: In (2,(dom <*X,Y*>)) = 2 by SUBSET_1:def 8;
X1: f * (reproj1 z) = f * (((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z)))) by LM180
.= g * (reproj ((In (1,(dom <*X,Y*>))),w)) by RELAT_1:36 ;
X3: X = <*X,Y*> . (In (1,(dom <*X,Y*>))) by AS1;
Y1: f * (reproj2 z) = f * (((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z)))) by LM180
.= g * (reproj ((In (2,(dom <*X,Y*>))),w)) by RELAT_1:36 ;
Y3: Y = <*X,Y*> . (In (2,(dom <*X,Y*>))) by AS2;
thus partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) by X1, X3, LM190; :: thesis: partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2)
thus partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) by Y1, Y3, LM190; :: thesis: verum