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_{1} being set holds

( not i in dom (G ** F) or not (G ** F) . i = b_{1} or b_{1} 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

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

( not i in dom (G ** F) or not (G ** F) . i = b

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