let X, Y, W be RealNormSpace; :: thesis: for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_in`1 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies f is_partial_differentiable_in`1 z ) & ( f is_partial_differentiable_in`2 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies f is_partial_differentiable_in`2 z ) )
let z be Point of [:X,Y:]; :: thesis: for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_in`1 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies f is_partial_differentiable_in`1 z ) & ( f is_partial_differentiable_in`2 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies f is_partial_differentiable_in`2 z ) )
let f be PartFunc of [:X,Y:],W; :: thesis: ( ( f is_partial_differentiable_in`1 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies f is_partial_differentiable_in`1 z ) & ( f is_partial_differentiable_in`2 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies f is_partial_differentiable_in`2 z ) )
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, FINSEQ_1:44;
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, FINSEQ_1:44;
thus ( f is_partial_differentiable_in`1 z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) by X1, X3, LM190; :: thesis: ( f is_partial_differentiable_in`2 z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 )
thus ( f is_partial_differentiable_in`2 z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) by Y1, Y3, LM190; :: thesis: verum