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"

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

hence
G ** F is "onto"
; :: thesis: verumrng ((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;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