[:P,Q:] is bijective
_{1} being Function of [:A,B:],[:A,B:] st b_{1} = [:P,Q:] holds

b_{1} is bijective
; :: thesis: verum

proof

hence
for b
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;( 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

b