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 st F is "onto" & G is "onto" holds
G ** F is "onto"
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 st F is "onto" & G is "onto" holds
G ** F is "onto"
let B, C be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"
let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"
let G be ManySortedFunction of B,C; :: thesis: ( F is "onto" & G is "onto" implies G ** F is "onto" )
assume A1: ( F is "onto" & G is "onto" ) ; :: thesis: G ** F is "onto"

now :: thesis: for i being set st i in I holds
rng ((G ** F) . i) = C . i

let i be set ; :: thesis: ( i in I implies rng ((G ** F) . i) = C . i )
assume A2: i in I ; :: thesis: rng ((G ** F) . i) = C . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
reconsider g = G . i as Function of (B . i),(C . i) by A2, PBOOLE:def 15;
( rng f = B . i & rng g = C . i ) by A1, A2;
then rng (g * f) = C . i by A2, FUNCT_2:14;
hence rng ((G ** F) . i) = C . i by A2, MSUALG_3:2; :: thesis: verum

end;

hence G ** F is "onto" ; :: thesis: verum