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 st F is "onto" & G is "onto" holds
G ** F is "onto"
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 st F is "onto" & G is "onto" holds
G ** F is "onto"
let B, C be V2() ManySortedSet of ; :: 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 that
A1: F is "onto" and
A2: G is "onto" ; :: thesis: G ** F is "onto"

now

let i be set ; :: thesis: ( i in I implies rng ((G ** F) . i) = C . i )
assume A3: 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 18;
reconsider g = G . i as Function of (B . i),(C . i) by A3, PBOOLE:def 18;
( rng f = B . i & rng g = C . i ) by A1, A2, A3, MSUALG_3:def 3;
then rng (g * f) = C . i by A3, FUNCT_2:20;
hence rng ((G ** F) . i) = C . i by A3, MSUALG_3:2; :: thesis: verum

end;

hence G ** F is "onto" by MSUALG_3:def 3; :: thesis: verum