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[ set , set , set ] 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]] );
P1: for x, y being set st x in [:D,E:] & y in [:F,G:] holds
ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] )
proof
let x, y be set ; :: thesis: ( x in [:D,E:] & y in [:F,G:] implies ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) )
assume AS: ( x in [:D,E:] & y in [:F,G:] ) ; :: thesis: ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] )
consider d, e being set such that
AS1: ( d in D & e in E & x = [d,e] ) by ZFMISC_1:def 2, AS;
consider f, g being set such that
AS2: ( f in F & g in G & y = [f,g] ) by ZFMISC_1:def 2, AS;
( [d,f] in [:D,F:] & [e,g] in [:E,G:] ) by AS1, AS2, ZFMISC_1:106;
then [[d,f],[e,g]] in [:[:D,F:],[:E,G:]:] by ZFMISC_1:106;
hence ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) by AS1, AS2; :: thesis: verum
end;
consider I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] such that
P2: for x, y being set st x in [:D,E:] & y in [:F,G:] holds
S1[x,y,I . (x,y)] from BINOP_1:sch 1(P1);
 AP5: 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 AS1: ( d in D & e in E & f in F & g in G ) ; :: thesis: I . ([d,e],[f,g]) = [[d,f],[e,g]]
PP1: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by AS1, ZFMISC_1:106;
consider d1, e1, f1, g1 being set such that
PP3: ( 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 PP1, P2;
( d1 = d & e1 = e & f1 = f & g1 = g ) by PP3, ZFMISC_1:33;
hence I . ([d,e],[f,g]) = [[d,f],[e,g]] by PP3; :: thesis: verum
end;
AP6: I is one-to-one
proof
now
let z1, z2 be set ; :: thesis: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 implies z1 = z2 )
assume P3: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
consider de1, fg1 being set such that
P4: ( de1 in [:D,E:] & fg1 in [:F,G:] & z1 = [de1,fg1] ) by ZFMISC_1:def 2, P3;
consider d1, e1 being set such that
P5: ( d1 in D & e1 in E & de1 = [d1,e1] ) by ZFMISC_1:def 2, P4;
consider f1, g1 being set such that
P6: ( f1 in F & g1 in G & fg1 = [f1,g1] ) by ZFMISC_1:def 2, P4;
consider de2, fg2 being set such that
Q4: ( de2 in [:D,E:] & fg2 in [:F,G:] & z2 = [de2,fg2] ) by ZFMISC_1:def 2, P3;
consider d2, e2 being set such that
Q5: ( d2 in D & e2 in E & de2 = [d2,e2] ) by ZFMISC_1:def 2, Q4;
consider f2, g2 being set such that
Q6: ( f2 in F & g2 in G & fg2 = [f2,g2] ) by ZFMISC_1:def 2, Q4;
[[d1,f1],[e1,g1]] = I . ([d1,e1],[f1,g1]) by AP5, P5, P6
.= I . ([d2,e2],[f2,g2]) by P3, P4, P5, P6, Q4, Q5, Q6
.= [[d2,f2],[e2,g2]] by AP5, Q5, Q6 ;
then ( [d1,f1] = [d2,f2] & [e1,g1] = [e2,g2] ) by ZFMISC_1:33;
then ( d1 = d2 & f1 = f2 & e1 = e2 & g1 = g2 ) by ZFMISC_1:33;
hence z1 = z2 by P4, P5, P6, Q4, Q5, Q6; :: thesis: verum
end;
hence I is one-to-one by FUNCT_2:25; :: thesis: verum
end;
I is onto
proof
now
let w be set ; :: thesis: ( w in [:[:D,F:],[:E,G:]:] implies w in rng I )
assume P3: w in [:[:D,F:],[:E,G:]:] ; :: thesis: w in rng I
consider df, eg being set such that
P4: ( df in [:D,F:] & eg in [:E,G:] & w = [df,eg] ) by ZFMISC_1:def 2, P3;
consider d, f being set such that
P5: ( d in D & f in F & df = [d,f] ) by ZFMISC_1:def 2, P4;
consider e, g being set such that
P6: ( e in E & g in G & eg = [e,g] ) by ZFMISC_1:def 2, P4;
PP1: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by P5, P6, ZFMISC_1:106;
reconsider z = [[d,e],[f,g]] as Element of [:[:D,E:],[:F,G:]:] by PP1, ZFMISC_1:106;
w = I . ([d,e],[f,g]) by AP5, P4, P5, P6;
then w = I . z ;
hence w in rng I by FUNCT_2:189; :: 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 AP5, AP6; :: thesis: verum