let n be non zero Nat; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for q being Element of REAL holds
( (ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ") is PartFunc of (REAL n),REAL & dom ((ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ")) = (CarProd ((Seg n) --> REAL)) .: (dom (ProjPMap2 (|.g.|,q))) )
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for q being Element of REAL holds
( (ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ") is PartFunc of (REAL n),REAL & dom ((ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ")) = (CarProd ((Seg n) --> REAL)) .: (dom (ProjPMap2 (|.g.|,q))) )
let q be Element of REAL ; :: thesis: ( (ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ") is PartFunc of (REAL n),REAL & dom ((ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ")) = (CarProd ((Seg n) --> REAL)) .: (dom (ProjPMap2 (|.g.|,q))) )
set P2 = ProjPMap2 (|.g.|,q);
A1: CarProd ((Seg n) --> REAL) is bijective by MEASUR14:12;
consider T being Function of (product ((Seg n) --> REAL)),(CarProduct ((Seg n) --> REAL)) such that
A2: ( T is bijective & T = (CarProd ((Seg n) --> REAL)) " & .: T = (.: (CarProd ((Seg n) --> REAL))) " ) by MEASUR14:12, MEASUR14:14;
(ProjPMap2 (|.g.|,q)) * T is PartFunc of (REAL n),REAL by SRINGS_5:8;
hence (ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ") is PartFunc of (REAL n),REAL by A2; :: thesis: dom ((ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ")) = (CarProd ((Seg n) --> REAL)) .: (dom (ProjPMap2 (|.g.|,q)))
dom ((ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ")) = T " (dom (ProjPMap2 (|.g.|,q))) by A2, RELAT_1:147;
hence dom ((ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ")) = (CarProd ((Seg n) --> REAL)) .: (dom (ProjPMap2 (|.g.|,q))) by A1, A2, FUNCT_1:84; :: thesis: verum