let I be set ; :: thesis: for A being ManySortedSet of
for B, C being V2() ManySortedSet of
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
let A be ManySortedSet of ; :: thesis: for B, C being V2() ManySortedSet of
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
let B, C be V2() ManySortedSet of ; :: thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
let G be ManySortedFunction of B,C; :: thesis: for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
let X be ManySortedSubset of A; :: thesis: (G ** F) || X = G ** (F || X)
now let i be
set ;
:: thesis: ( i in I implies ((G ** F) || X) . i = (G ** (F || X)) . i )assume A1:
i in I
;
:: thesis: ((G ** F) || X) . i = (G ** (F || X)) . ithen reconsider gf =
(G ** F) . i as
Function of
(A . i),
(C . i) by PBOOLE:def 18;
reconsider f =
F . i as
Function of
(A . i),
(B . i) by A1, PBOOLE:def 18;
reconsider g =
G . i as
Function of
(B . i),
(C . i) by A1, PBOOLE:def 18;
reconsider fx =
(F || X) . i as
Function of
(X . i),
(B . i) by A1, PBOOLE:def 18;
thus ((G ** F) || X) . i =
gf | (X . i)
by A1, MSAFREE:def 1
.=
(g * f) | (X . i)
by A1, MSUALG_3:2
.=
g * (f | (X . i))
by RELAT_1:112
.=
g * fx
by A1, MSAFREE:def 1
.=
(G ** (F || X)) . i
by A1, MSUALG_3:2
;
:: thesis: verum end;
hence
(G ** F) || X = G ** (F || X)
by PBOOLE:3; :: thesis: verum