let G1, G2, H1, H2 be non empty multMagma ; :: thesis: for f being Function of G1,H1
for g being Function of G2,H2 st f is onto & g is onto holds
Gr2Iso f,g is onto
let f be Function of G1,H1; :: thesis: for g being Function of G2,H2 st f is onto & g is onto holds
Gr2Iso f,g is onto
let g be Function of G2,H2; :: thesis: ( f is onto & g is onto implies Gr2Iso f,g is onto )
assume that
A1: rng f = the carrier of H1 and
A2: rng g = the carrier of H2 ; :: according to FUNCT_2:def 3 :: thesis: Gr2Iso f,g is onto
set h = Gr2Iso f,g;
thus rng (Gr2Iso f,g) c= the carrier of (product <*H1,H2*>) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (product <*H1,H2*>) c= proj2 (Gr2Iso f,g)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (product <*H1,H2*>) or a in proj2 (Gr2Iso f,g) )
assume a in the carrier of (product <*H1,H2*>) ; :: thesis: a in proj2 (Gr2Iso f,g)
then consider x being Element of H1, y being Element of H2 such that
A3: a = <*x,y*> by Th1;
consider a2 being set such that
A4: a2 in dom g and
A5: g . a2 = y by A2, FUNCT_1:def 5;
consider a1 being set such that
A6: a1 in dom f and
A7: f . a1 = x by A1, FUNCT_1:def 5;
( dom (Gr2Iso f,g) = the carrier of (product <*G1,G2*>) & ( for g being Element of G1
for h being Element of G2 holds <*g,h*> in the carrier of (product <*G1,G2*>) ) ) by FUNCT_2:def 1;
then A8: <*a1,a2*> in dom (Gr2Iso f,g) by A6, A4;
then consider k1 being Element of G1, k2 being Element of G2 such that
A9: <*a1,a2*> = <*k1,k2*> and
A10: (Gr2Iso f,g) . <*a1,a2*> = <*(f . k1),(g . k2)*> by Def1;
( a1 = k1 & a2 = k2 ) by A9, FINSEQ_1:98;
hence a in proj2 (Gr2Iso f,g) by A3, A7, A5, A8, A10, FUNCT_1:def 5; :: thesis: verum