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

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