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 non-empty ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F
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 non-empty ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F
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 non-empty ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F
let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C
for X being non-empty ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F
let G be ManySortedFunction of B,C; :: thesis: for X being non-empty ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F
let X be non-empty ManySortedSubset of B; :: thesis: ( rngs F c= X implies (G || X) ** F = G ** F )
assume A1: rngs F c= X ; :: thesis: (G || X) ** F = G ** F
A2: dom F = I by PARTFUN1:def 2;
A3: F is ManySortedFunction of A,X

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or F . i is Element of K19(K20((A . i),(X . i))) )
assume A4: i in I ; :: thesis: F . i is Element of K19(K20((A . i),(X . i)))
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
A5: (rngs F) . i c= X . i by A1, A4;
( dom f = A . i & (rngs F) . i = rng f ) by A2, A4, FUNCT_2:def 1, FUNCT_6:22;
hence F . i is Element of K19(K20((A . i),(X . i))) by A4, A5, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;

A6: now :: thesis: for i being object st i in I holds
((G || X) ** F) . i = (G ** F) . i

let i be object ; :: thesis: ( i in I implies ((G || X) ** F) . i = (G ** F) . i )
assume A7: i in I ; :: thesis: ((G || X) ** F) . i = (G ** F) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
(rngs F) . i = rng f by A2, A7, FUNCT_6:22;
then A8: rng f c= X . i by A1, A7;
dom f = A . i by A7, FUNCT_2:def 1;
then reconsider f9 = f as Function of (A . i),(X . i) by A7, A8, FUNCT_2:def 1, RELSET_1:4;
reconsider g = G . i as Function of (B . i),(C . i) by A7, PBOOLE:def 15;
A9: rng f9 c= X . i by RELAT_1:def 19;
reconsider gx = (G || X) . i as Function of (X . i),(C . i) by A7, PBOOLE:def 15;
thus ((G || X) ** F) . i = gx * f9 by A3, A7, MSUALG_3:2
.= (g | (X . i)) * f by A7, MSAFREE:def 1
.= g * f9 by A9, MSUHOM_1:1
.= (G ** F) . i by A7, MSUALG_3:2 ; :: thesis: verum

end;

(G || X) ** F is ManySortedSet of I by A3, Lm1;
hence (G || X) ** F = G ** F by A6, PBOOLE:3; :: thesis: verum