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 g ** f is "onto" holds
g 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 g ** f is "onto" holds
g 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 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 proj2 (g . i) = C . i )
assume A2: i in I ; :: thesis: proj2 (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 15;
rng ((g . i) * (f . i)) = rng ((g ** f) . i) by A2, MSUALG_3:2
.= C . i by A1, A2 ;
hence proj2 (g . i) = C . i by A2, A3, Th1; :: thesis: verum