[:P,Q:] is bijective
proof
thus [:P,Q:] is one-to-one ; :: according to FUNCT_2:def 4 :: thesis: [:P,Q:] is onto
( rng P = A & rng Q = B ) by FUNCT_2:def 3;
hence rng [:P,Q:] = [:A,B:] by FUNCT_3:67; :: according to FUNCT_2:def 3 :: thesis: verum
end;
hence for b1 being Function of [:A,B:],[:A,B:] st b1 = [:P,Q:] holds
b1 is bijective ; :: thesis: verum