let F, G be Function-yielding Function; :: thesis: ( F is "1-1" & G is "1-1" implies G ** F is "1-1" )
assume A1: ( F is "1-1" & G is "1-1" ) ; :: thesis: G ** F is "1-1"
let i be set ; :: according to MSUALG_3:def 2 :: thesis: for b₁ being set holds
( not i in dom (G ** F) or not (G ** F) . i = b₁ or b₁ is one-to-one )
let f be Function; :: thesis: ( not i in dom (G ** F) or not (G ** F) . i = f or f is one-to-one )
assume that
A2: i in dom (G ** F) and
A3: (G ** F) . i = f ; :: thesis: f is one-to-one
dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def 24;
then ( i in dom G & i in dom F ) by A2, XBOOLE_0:def 4;
then ( G . i is one-to-one & F . i is one-to-one ) by A1, MSUALG_3:def 2;
then (G . i) * (F . i) is one-to-one ;
hence f is one-to-one by A2, A3, PBOOLE:def 24; :: thesis: verum