let X, Z be non empty TopSpace; :: thesis: for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)

let Y be non empty SubSpace of Z; :: thesis: oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)

set XY = oContMaps (X,Y);

set XZ = oContMaps (X,Z);

A1: Omega Y is full SubRelStr of Omega Z by WAYBEL25:17;

A2: [#] Y c= [#] Z by PRE_TOPC:def 4;

oContMaps (X,Y) is SubRelStr of oContMaps (X,Z)

A5: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY = the InternalRel of (oContMaps (X,Z)) /\ [: the carrier of XY, the carrier of XY:] by WELLORD1:def 6;

the InternalRel of XY = the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY

let Y be non empty SubSpace of Z; :: thesis: oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)

set XY = oContMaps (X,Y);

set XZ = oContMaps (X,Z);

A1: Omega Y is full SubRelStr of Omega Z by WAYBEL25:17;

A2: [#] Y c= [#] Z by PRE_TOPC:def 4;

oContMaps (X,Y) is SubRelStr of oContMaps (X,Z)

proof

then reconsider XY = oContMaps (X,Y) as non empty SubRelStr of oContMaps (X,Z) ;
thus A3:
the carrier of (oContMaps (X,Y)) c= the carrier of (oContMaps (X,Z))
:: according to YELLOW_0:def 13 :: thesis: the InternalRel of (oContMaps (X,Y)) c= the InternalRel of (oContMaps (X,Z))

assume A4: [x,y] in the InternalRel of (oContMaps (X,Y)) ; :: thesis: [x,y] in the InternalRel of (oContMaps (X,Z))

reconsider x = x, y = y as Element of (oContMaps (X,Y)) by A4, ZFMISC_1:87;

reconsider a = x, b = y as Element of (oContMaps (X,Z)) by A3;

reconsider f = x, g = y as continuous Function of X,(Omega Y) by Th1;

reconsider f9 = a, g9 = b as continuous Function of X,(Omega Z) by Th1;

x <= y by A4, ORDERS_2:def 5;

then f <= g by Th3;

then f9 <= g9 by A1, YELLOW16:2;

then a <= b by Th3;

hence [x,y] in the InternalRel of (oContMaps (X,Z)) by ORDERS_2:def 5; :: thesis: verum

end;proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of (oContMaps (X,Y)) or [x,y] in the InternalRel of (oContMaps (X,Z)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (oContMaps (X,Y)) or x in the carrier of (oContMaps (X,Z)) )

assume x in the carrier of (oContMaps (X,Y)) ; :: thesis: x in the carrier of (oContMaps (X,Z))

then reconsider f = x as continuous Function of X,Y by Th2;

( dom f = the carrier of X & rng f c= the carrier of Z ) by A2, FUNCT_2:def 1;

then x is continuous Function of X,Z by FUNCT_2:2, PRE_TOPC:26;

then x is Element of (oContMaps (X,Z)) by Th2;

hence x in the carrier of (oContMaps (X,Z)) ; :: thesis: verum

end;assume x in the carrier of (oContMaps (X,Y)) ; :: thesis: x in the carrier of (oContMaps (X,Z))

then reconsider f = x as continuous Function of X,Y by Th2;

( dom f = the carrier of X & rng f c= the carrier of Z ) by A2, FUNCT_2:def 1;

then x is continuous Function of X,Z by FUNCT_2:2, PRE_TOPC:26;

then x is Element of (oContMaps (X,Z)) by Th2;

hence x in the carrier of (oContMaps (X,Z)) ; :: thesis: verum

assume A4: [x,y] in the InternalRel of (oContMaps (X,Y)) ; :: thesis: [x,y] in the InternalRel of (oContMaps (X,Z))

reconsider x = x, y = y as Element of (oContMaps (X,Y)) by A4, ZFMISC_1:87;

reconsider a = x, b = y as Element of (oContMaps (X,Z)) by A3;

reconsider f = x, g = y as continuous Function of X,(Omega Y) by Th1;

reconsider f9 = a, g9 = b as continuous Function of X,(Omega Z) by Th1;

x <= y by A4, ORDERS_2:def 5;

then f <= g by Th3;

then f9 <= g9 by A1, YELLOW16:2;

then a <= b by Th3;

hence [x,y] in the InternalRel of (oContMaps (X,Z)) by ORDERS_2:def 5; :: thesis: verum

A5: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY = the InternalRel of (oContMaps (X,Z)) /\ [: the carrier of XY, the carrier of XY:] by WELLORD1:def 6;

the InternalRel of XY = the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY

proof

hence
oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
by YELLOW_0:def 14; :: thesis: verum
the InternalRel of XY c= the InternalRel of (oContMaps (X,Z))
by YELLOW_0:def 13;

hence the InternalRel of XY c= the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY by A5, XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY c= the InternalRel of XY

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY or [x,y] in the InternalRel of XY )

assume A6: [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY ; :: thesis: [x,y] in the InternalRel of XY

then A7: [x,y] in [: the carrier of XY, the carrier of XY:] by A5, XBOOLE_0:def 4;

reconsider x = x, y = y as Element of XY by A7, ZFMISC_1:87;

the carrier of XY c= the carrier of (oContMaps (X,Z)) by YELLOW_0:def 13;

then reconsider a = x, b = y as Element of (oContMaps (X,Z)) ;

reconsider f9 = a, g9 = b as continuous Function of X,(Omega Z) by Th1;

reconsider f = x, g = y as continuous Function of X,(Omega Y) by Th1;

[a,b] in the InternalRel of (oContMaps (X,Z)) by A5, A6, XBOOLE_0:def 4;

then a <= b by ORDERS_2:def 5;

then f9 <= g9 by Th3;

then f <= g by A1, YELLOW16:3;

then x <= y by Th3;

hence [x,y] in the InternalRel of XY by ORDERS_2:def 5; :: thesis: verum

end;hence the InternalRel of XY c= the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY by A5, XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY c= the InternalRel of XY

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY or [x,y] in the InternalRel of XY )

assume A6: [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY ; :: thesis: [x,y] in the InternalRel of XY

then A7: [x,y] in [: the carrier of XY, the carrier of XY:] by A5, XBOOLE_0:def 4;

reconsider x = x, y = y as Element of XY by A7, ZFMISC_1:87;

the carrier of XY c= the carrier of (oContMaps (X,Z)) by YELLOW_0:def 13;

then reconsider a = x, b = y as Element of (oContMaps (X,Z)) ;

reconsider f9 = a, g9 = b as continuous Function of X,(Omega Z) by Th1;

reconsider f = x, g = y as continuous Function of X,(Omega Y) by Th1;

[a,b] in the InternalRel of (oContMaps (X,Z)) by A5, A6, XBOOLE_0:def 4;

then a <= b by ORDERS_2:def 5;

then f9 <= g9 by Th3;

then f <= g by A1, YELLOW16:3;

then x <= y by Th3;

hence [x,y] in the InternalRel of XY by ORDERS_2:def 5; :: thesis: verum