let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL-NS n)
for X being set st ( for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | X is constant ) holds
f | X is constant
let f be PartFunc of REAL,(REAL-NS n); :: thesis: for X being set st ( for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | X is constant ) holds
f | X is constant
let X be set ; :: thesis: ( ( for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | X is constant ) implies f | X is constant )
assume A1: for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | X is constant ; :: thesis: f | X is constant
A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

now :: thesis: for x, y being object st x in dom (f | X) & y in dom (f | X) holds
(f | X) . x = (f | X) . y

let x, y be object ; :: thesis: ( x in dom (f | X) & y in dom (f | X) implies (f | X) . x = (f | X) . y )
assume A3: ( x in dom (f | X) & y in dom (f | X) ) ; :: thesis: (f | X) . x = (f | X) . y
then A4: ( x in dom f & x in X & y in dom f & y in X ) by RELAT_1:57;
f . x in rng f by A4, FUNCT_1:3;
then reconsider fx = f . x as Element of REAL n by REAL_NS1:def 4;
f . y in rng f by A4, FUNCT_1:3;
then reconsider fy = f . y as Element of REAL n by REAL_NS1:def 4;
A5: len fy = n by CARD_1:def 7;
A6: len fx = n by CARD_1:def 7;

now :: thesis: for i being Nat st 1 <= i & i <= len fx holds
fx . i = fy . i

let i be Nat; :: thesis: ( 1 <= i & i <= len fx implies fx . i = fy . i )
assume A7: ( 1 <= i & i <= len fx ) ; :: thesis: fx . i = fy . i
dom (proj (i,n)) = the carrier of (REAL-NS n) by A2, FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A8: dom f = dom ((proj (i,n)) * f) by RELAT_1:27;
A9: (((proj (i,n)) * f) | X) . x = ((proj (i,n)) * f) . x by A3, FUNCT_1:49
.= (proj (i,n)) . (f . x) by A4, FUNCT_1:13
.= fx . i by PDIFF_1:def 1 ;
A10: (((proj (i,n)) * f) | X) . y = ((proj (i,n)) * f) . y by A3, FUNCT_1:49
.= (proj (i,n)) . (f . y) by A4, FUNCT_1:13
.= fy . i by PDIFF_1:def 1 ;
A11: ((proj (i,n)) * f) | X is constant by A1, A7, A6;
( x in dom (((proj (i,n)) * f) | X) & y in dom (((proj (i,n)) * f) | X) ) by A8, A4, RELAT_1:57;
hence fx . i = fy . i by A9, A10, A11, FUNCT_1:def 10; :: thesis: verum

end;

then A12: fx = fy by A5, CARD_1:def 7;
thus (f | X) . x = f . x by A3, FUNCT_1:49
.= (f | X) . y by A3, A12, FUNCT_1:49 ; :: thesis: verum

end;

hence f | X is constant by FUNCT_1:def 10; :: thesis: verum