let J, A, B be non empty set ; :: thesis: for K being ManySortedSet of J
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 J; :: 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:59
.= J by MSUALG_3:2 ;

A2: now :: thesis: for x being object st x in J holds
(doms ((J => f) ** F)) . x = (doms F) . x

let x be object ; :: 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: j in dom F by A3, PARTFUN1:def 2;
A5: ( rng (F . j) c= A & dom f = A ) by FUNCT_2:def 1;
j in dom ((J => f) ** F) by A1, A3, FUNCT_6:59;
then (doms ((J => f) ** F)) . j = dom (((J => f) ** F) . j) by FUNCT_6:22
.= dom (((J => f) . j) * (F . j)) by MSUALG_3:2
.= dom (f * (F . j))
.= dom (F . j) by A5, RELAT_1:27
.= (doms F) . j by A4, FUNCT_6:22 ;
hence (doms ((J => f) ** F)) . x = (doms F) . x ; :: thesis: verum

end;

dom (doms F) = dom F by FUNCT_6:59
.= J by PARTFUN1:def 2 ;
hence doms ((J => f) ** F) = doms F by A1, A2, FUNCT_1:2; :: thesis: verum