let I be set ; :: thesis: for A being ManySortedSet of I
for B, C being V2() ManySortedSet of
for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let A be ManySortedSet of I; :: thesis: for B, C being V2() ManySortedSet of
for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g 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 g ** f is "onto" holds
g is "onto"
let f be ManySortedFunction of A,B; :: thesis: for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let g be ManySortedFunction of B,C; :: thesis: ( g ** f is "onto" implies g is "onto" )
assume A1: g ** f is "onto" ; :: thesis: g is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in I or rng (g . i) = C . i )
assume A2: i in I ; :: thesis: rng (g . i) = C . i
then A3: ( f . i is Function of A . i,B . i & g . i is Function of B . i,C . i ) by PBOOLE:def 18;
rng ((g . i) * (f . i)) = rng ((g ** f) . i) by A2, MSUALG_3:2
.= C . i by A1, A2, MSUALG_3:def 3 ;
hence rng (g . i) = C . i by A2, A3, Th1; :: thesis: verum