let I be set ; :: thesis: for A being ManySortedSet of I
for B, C being V2() 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 V2() 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 V2() 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 ;
( rng f = B . i & rng g = C . i ) by A1, A2;
then rng (g * f) = C . i by ;
hence rng ((G ** F) . i) = C . i by ; :: thesis: verum
end;
hence G ** F is "onto" ; :: thesis: verum