let T be non empty TopSpace-like unital BinContinuous TopGrStr ; :: thesis: for F, G being Function of [:I[01],I[01]:],T
for M, N being Subset of [:I[01],I[01]:] holds (HomotopyMlt (F,G)) .: (M /\ N) c= (F .: M) * (G .: N)
let F, G be Function of [:I[01],I[01]:],T; :: thesis: for M, N being Subset of [:I[01],I[01]:] holds (HomotopyMlt (F,G)) .: (M /\ N) c= (F .: M) * (G .: N)
let M, N be Subset of [:I[01],I[01]:]; :: thesis: (HomotopyMlt (F,G)) .: (M /\ N) c= (F .: M) * (G .: N)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (HomotopyMlt (F,G)) .: (M /\ N) or y in (F .: M) * (G .: N) )
assume y in (HomotopyMlt (F,G)) .: (M /\ N) ; :: thesis: y in (F .: M) * (G .: N)
then consider x being Point of [:I[01],I[01]:] such that
A1: x in M /\ N and
A2: (HomotopyMlt (F,G)) . x = y by FUNCT_2:65;
consider a, b being Point of I[01] such that
A3: x = [a,b] by BORSUK_1:10;
A4: (HomotopyMlt (F,G)) . (a,b) = (F . (a,b)) * (G . (a,b)) by Def7;
( [a,b] in M & [a,b] in N ) by A1, A3, XBOOLE_0:def 4;
then ( F . (a,b) in F .: M & G . (a,b) in G .: N ) by FUNCT_2:35;
hence y in (F .: M) * (G .: N) by A2, A3, A4; :: thesis: verum