theorem :: PRVECT_3:1

for D, E, F, G being non empty set 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]] ) )