let i be Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL i),REAL st Z c= dom f holds
dom ((<>* f) | Z) = Z
let Z be set ; :: thesis: for f being PartFunc of (REAL i),REAL st Z c= dom f holds
dom ((<>* f) | Z) = Z
let f be PartFunc of (REAL i),REAL; :: thesis: ( Z c= dom f implies dom ((<>* f) | Z) = Z )
assume Z c= dom f ; :: thesis: dom ((<>* f) | Z) = Z
then Z c= dom (<>* f) by Th3;
hence dom ((<>* f) | Z) = Z by RELAT_1:62; :: thesis: verum