let I be set ; :: thesis: for F, G being ManySortedFunction of
for A being ManySortedSet of st A in doms G holds
F .. (G .. A) = (F ** G) .. A
let F, G be ManySortedFunction of ; :: thesis: for A being ManySortedSet of st A in doms G holds
F .. (G .. A) = (F ** G) .. A
let A be ManySortedSet of ; :: thesis: ( A in doms G implies F .. (G .. A) = (F ** G) .. A )
assume A1:
A in doms G
; :: thesis: F .. (G .. A) = (F ** G) .. A
A2:
dom F = I
by PARTFUN1:def 4;
A3:
dom G = I
by PARTFUN1:def 4;
reconsider FG = F ** G as ManySortedFunction of by MSSUBFAM:15;
A4:
dom FG = I
by PARTFUN1:def 4;
A5:
FG .. A is ManySortedSet of
;
now let i be
set ;
:: thesis: ( i in I implies (F .. (G .. A)) . i = ((F ** G) .. A) . i )assume A6:
i in I
;
:: thesis: (F .. (G .. A)) . i = ((F ** G) .. A) . ireconsider f =
F . i as
Function ;
reconsider g =
G . i as
Function ;
reconsider fg =
(F ** G) . i as
Function ;
dom g = (doms G) . i
by A6, MSSUBFAM:14;
then A7:
A . i in dom g
by A1, A6, PBOOLE:def 4;
(G .. A) . i = g . (A . i)
by A3, A6, PRALG_1:def 17;
hence (F .. (G .. A)) . i =
f . (g . (A . i))
by A2, A6, PRALG_1:def 17
.=
(f * g) . (A . i)
by A7, FUNCT_1:23
.=
fg . (A . i)
by A4, A6, PBOOLE:def 24
.=
((F ** G) .. A) . i
by A4, A6, PRALG_1:def 17
;
:: thesis: verum end;
hence
F .. (G .. A) = (F ** G) .. A
by A5, PBOOLE:3; :: thesis: verum