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 ;

.= J by PARTFUN1:def 2 ;

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

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

dom (doms F) =
dom F
by FUNCT_6:59
(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;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

.= J by PARTFUN1:def 2 ;

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