let X1, X2, Y be non empty set ; :: thesis: for F being Functional_Sequence of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 st F is with_the_same_dom holds
( ProjPMap1 (F,x) is with_the_same_dom & ProjPMap2 (F,y) is with_the_same_dom )
let F be Functional_Sequence of [:X1,X2:],Y; :: thesis: for x being Element of X1
for y being Element of X2 st F is with_the_same_dom holds
( ProjPMap1 (F,x) is with_the_same_dom & ProjPMap2 (F,y) is with_the_same_dom )
let x1 be Element of X1; :: thesis: for y being Element of X2 st F is with_the_same_dom holds
( ProjPMap1 (F,x1) is with_the_same_dom & ProjPMap2 (F,y) is with_the_same_dom )
let x2 be Element of X2; :: thesis: ( F is with_the_same_dom implies ( ProjPMap1 (F,x1) is with_the_same_dom & ProjPMap2 (F,x2) is with_the_same_dom ) )
assume A1: F is with_the_same_dom ; :: thesis: ( ProjPMap1 (F,x1) is with_the_same_dom & ProjPMap2 (F,x2) is with_the_same_dom )
now :: thesis: for m, n being Nat holds dom ((ProjPMap1 (F,x1)) . m) = dom ((ProjPMap1 (F,x1)) . n)
let m, n be Nat; :: thesis: dom ((ProjPMap1 (F,x1)) . m) = dom ((ProjPMap1 (F,x1)) . n)
dom ((ProjPMap1 (F,x1)) . m) = dom (ProjPMap1 ((F . m),x1)) by Def5
.= X-section ((dom (F . m)),x1) by Def3
.= X-section ((dom (F . n)),x1) by A1, MESFUNC8:def 2
.= dom (ProjPMap1 ((F . n),x1)) by Def3 ;
hence dom ((ProjPMap1 (F,x1)) . m) = dom ((ProjPMap1 (F,x1)) . n) by Def5; :: thesis: verum
end;
hence ProjPMap1 (F,x1) is with_the_same_dom by MESFUNC8:def 2; :: thesis: ProjPMap2 (F,x2) is with_the_same_dom
now :: thesis: for m, n being Nat holds dom ((ProjPMap2 (F,x2)) . m) = dom ((ProjPMap2 (F,x2)) . n)
let m, n be Nat; :: thesis: dom ((ProjPMap2 (F,x2)) . m) = dom ((ProjPMap2 (F,x2)) . n)
dom ((ProjPMap2 (F,x2)) . m) = dom (ProjPMap2 ((F . m),x2)) by Def6
.= Y-section ((dom (F . m)),x2) by Def4
.= Y-section ((dom (F . n)),x2) by A1, MESFUNC8:def 2
.= dom (ProjPMap2 ((F . n),x2)) by Def4 ;
hence dom ((ProjPMap2 (F,x2)) . m) = dom ((ProjPMap2 (F,x2)) . n) by Def6; :: thesis: verum
end;
hence ProjPMap2 (F,x2) is with_the_same_dom by MESFUNC8:def 2; :: thesis: verum