let F, G be Function-yielding Function; :: thesis: ( F is "1-1" & G is "1-1" implies G ** F is "1-1" )
assume that
A1: F is "1-1" and
A2: 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
A3: i in dom (G ** F) and
A4: (G ** F) . i = f ; :: thesis: f is one-to-one
A5: dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def 19;
then i in dom F by A3, XBOOLE_0:def 4;
then A6: F . i is one-to-one by A1;
i in dom G by A3, A5, XBOOLE_0:def 4;
then G . i is one-to-one by A2;
then (G . i) * (F . i) is one-to-one by A6;
hence f is one-to-one by A3, A4, PBOOLE:def 19; :: thesis: verum