let I be set ; :: thesis: for A being ManySortedSet of I
for B, C being non-empty ManySortedSet of I
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 I; :: thesis: for B, C being non-empty ManySortedSet of I
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 non-empty ManySortedSet of I; :: 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 :: thesis: for i being object st i in I holds
((G ** F) || X) . i = (G ** (F || X)) . i

let i be object ; :: 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)) . i
then reconsider gf = (G ** F) . i as Function of (A . i),(C . i) by PBOOLE:def 15;
reconsider fx = (F || X) . i as Function of (X . i),(B . i) by A1, PBOOLE:def 15;
reconsider g = G . i as Function of (B . i),(C . i) by A1, PBOOLE:def 15;
reconsider f = F . i as Function of (A . i),(B . i) by A1, PBOOLE:def 15;
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:83
.= 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) ; :: thesis: verum