let J, A, B be non empty set ; :: thesis: for K being ManySortedSet of
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds doms ((J => f) ** F) = doms F
let K be ManySortedSet of ; :: thesis: for F being DoubleIndexedSet of K,A
for f being Function of A,B holds doms ((J => f) ** F) = doms F
let F be DoubleIndexedSet of K,A; :: thesis: for f being Function of A,B holds doms ((J => f) ** F) = doms F
let f be Function of A,B; :: thesis: doms ((J => f) ** F) = doms F
A1: dom (doms ((J => f) ** F)) = dom ((J => f) ** F) by FUNCT_6:89
.= J by MSUALG_3:2 ;
A2: dom (doms F) = dom F by FUNCT_6:89
.= J by PARTFUN1:def 4 ;

now

let x be set ; :: thesis: ( x in J implies (doms ((J => f) ** F)) . x = (doms F) . x )
assume A3: x in J ; :: thesis: (doms ((J => f) ** F)) . x = (doms F) . x
then reconsider j = x as Element of J ;
A4: ( rng (F . j) c= A & dom f = A ) by FUNCT_2:def 1;
A5: j in dom F by A3, PARTFUN1:def 4;
j in dom ((J => f) ** F) by A1, A3, FUNCT_6:89;
then (doms ((J => f) ** F)) . j = dom (((J => f) ** F) . j) by FUNCT_6:31
.= dom (((J => f) . j) * (F . j)) by MSUALG_3:2
.= dom (f * (F . j)) by FUNCOP_1:13
.= dom (F . j) by A4, RELAT_1:46
.= (doms F) . j by A5, FUNCT_6:31 ;
hence (doms ((J => f) ** F)) . x = (doms F) . x ; :: thesis: verum

end;

hence doms ((J => f) ** F) = doms F by A1, A2, FUNCT_1:9; :: thesis: verum