let D, E, F, G be non empty set ; :: thesis: ex I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] st
( I is one-to-one & I is onto & ( for d, e, f, g being set st d in D & e in E & f in F & g in G holds
I . ([d,e],[f,g]) = [[d,f],[e,g]] ) )
defpred S1[ object , object , object ] means ex d, e, f, g being set st
( d in D & e in E & f in F & g in G & $1 = [d,e] & $2 = [f,g] & $3 = [[d,f],[e,g]] );
A1: for x, y being object st x in [:D,E:] & y in [:F,G:] holds
ex z being object st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] )
proof
let x, y be object ; :: thesis: ( x in [:D,E:] & y in [:F,G:] implies ex z being object st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) )
assume A2: ( x in [:D,E:] & y in [:F,G:] ) ; :: thesis: ex z being object st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] )
consider d, e being object such that
A3: ( d in D & e in E & x = [d,e] ) by A2, ZFMISC_1:def 2;
consider f, g being object such that
A4: ( f in F & g in G & y = [f,g] ) by A2, ZFMISC_1:def 2;
( [d,f] in [:D,F:] & [e,g] in [:E,G:] ) by A3, A4, ZFMISC_1:87;
then [[d,f],[e,g]] in [:[:D,F:],[:E,G:]:] by ZFMISC_1:87;
hence ex z being object st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) by A3, A4; :: thesis: verum
end;
consider I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] such that
A5: for x, y being object st x in [:D,E:] & y in [:F,G:] holds
S1[x,y,I . (x,y)] from BINOP_1:sch 1(A1);
 A6: for d, e, f, g being set st d in D & e in E & f in F & g in G holds
I . ([d,e],[f,g]) = [[d,f],[e,g]]
proof
let d, e, f, g be set ; :: thesis: ( d in D & e in E & f in F & g in G implies I . ([d,e],[f,g]) = [[d,f],[e,g]] )
assume A7: ( d in D & e in E & f in F & g in G ) ; :: thesis: I . ([d,e],[f,g]) = [[d,f],[e,g]]
A8: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by A7, ZFMISC_1:87;
consider d1, e1, f1, g1 being set such that
A9: ( d1 in D & e1 in E & f1 in F & g1 in G & [d,e] = [d1,e1] & [f,g] = [f1,g1] & I . ([d,e],[f,g]) = [[d1,f1],[e1,g1]] ) by A8, A5;
( d1 = d & e1 = e & f1 = f & g1 = g ) by A9, XTUPLE_0:1;
hence I . ([d,e],[f,g]) = [[d,f],[e,g]] by A9; :: thesis: verum
end;
A10: I is one-to-one
proof
now :: thesis: for z1, z2 being object st z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 holds
z1 = z2
let z1, z2 be object ; :: thesis: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 implies z1 = z2 )
assume A11: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
consider de1, fg1 being object such that
A12: ( de1 in [:D,E:] & fg1 in [:F,G:] & z1 = [de1,fg1] ) by A11, ZFMISC_1:def 2;
consider d1, e1 being object such that
A13: ( d1 in D & e1 in E & de1 = [d1,e1] ) by A12, ZFMISC_1:def 2;
consider f1, g1 being object such that
A14: ( f1 in F & g1 in G & fg1 = [f1,g1] ) by A12, ZFMISC_1:def 2;
consider de2, fg2 being object such that
A15: ( de2 in [:D,E:] & fg2 in [:F,G:] & z2 = [de2,fg2] ) by A11, ZFMISC_1:def 2;
consider d2, e2 being object such that
A16: ( d2 in D & e2 in E & de2 = [d2,e2] ) by A15, ZFMISC_1:def 2;
consider f2, g2 being object such that
A17: ( f2 in F & g2 in G & fg2 = [f2,g2] ) by A15, ZFMISC_1:def 2;
[[d1,f1],[e1,g1]] = I . ([d1,e1],[f1,g1]) by A6, A13, A14
.= I . ([d2,e2],[f2,g2]) by A11, A12, A13, A14, A15, A16, A17
.= [[d2,f2],[e2,g2]] by A6, A16, A17 ;
then ( [d1,f1] = [d2,f2] & [e1,g1] = [e2,g2] ) by XTUPLE_0:1;
then ( d1 = d2 & f1 = f2 & e1 = e2 & g1 = g2 ) by XTUPLE_0:1;
hence z1 = z2 by A12, A13, A14, A15, A16, A17; :: thesis: verum
end;
hence I is one-to-one by FUNCT_2:19; :: thesis: verum
end;
I is onto
proof
now :: thesis: for w being object st w in [:[:D,F:],[:E,G:]:] holds
w in rng I
let w be object ; :: thesis: ( w in [:[:D,F:],[:E,G:]:] implies w in rng I )
assume A18: w in [:[:D,F:],[:E,G:]:] ; :: thesis: w in rng I
consider df, eg being object such that
A19: ( df in [:D,F:] & eg in [:E,G:] & w = [df,eg] ) by A18, ZFMISC_1:def 2;
consider d, f being object such that
A20: ( d in D & f in F & df = [d,f] ) by A19, ZFMISC_1:def 2;
consider e, g being object such that
A21: ( e in E & g in G & eg = [e,g] ) by A19, ZFMISC_1:def 2;
A22: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by A20, A21, ZFMISC_1:87;
reconsider z = [[d,e],[f,g]] as Element of [:[:D,E:],[:F,G:]:] by A22, ZFMISC_1:87;
w = I . ([d,e],[f,g]) by A6, A19, A20, A21;
then w = I . z ;
hence w in rng I by FUNCT_2:112; :: thesis: verum
end;
then [:[:D,F:],[:E,G:]:] c= rng I by TARSKI:def 3;
then [:[:D,F:],[:E,G:]:] = rng I by XBOOLE_0:def 10;
hence I is onto by FUNCT_2:def 3; :: thesis: verum
end;
hence ex I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] st
( I is one-to-one & I is onto & ( for d, e, f, g being set st d in D & e in E & f in F & g in G holds
I . ([d,e],[f,g]) = [[d,f],[e,g]] ) ) by A6, A10; :: thesis: verum