let n be Nat; :: thesis: RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #)
set V = RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #);
set W = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #);
A1: the carrier of RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) = REAL n by REAL_NS1:def 4
.= the carrier of RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) by EUCLID:22 ;
A2: RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by EUCLID:def 8;
A3: the ZeroF of RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) = 0. (REAL-NS n)
.= 0* n by REAL_NS1:def 4
.= 0. (RealVectSpace (Seg n)) by FINSEQ_2:def 2
.= the ZeroF of RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) by EUCLID:def 8 ;
A4: Funcs ((Seg n),REAL) = REAL n by FINSEQ_2:93;
for x, y being Element of REAL n holds (Euclid_add n) . (x,y) = (RealFuncAdd (Seg n)) . (x,y)
proof
let x, y be Element of REAL n; :: thesis: (Euclid_add n) . (x,y) = (RealFuncAdd (Seg n)) . (x,y)
reconsider x1 = x, y1 = y as Point of (TOP-REAL n) by A1, REAL_NS1:def 4;
thus (Euclid_add n) . (x,y) = x1 + y1 by REAL_NS1:def 1
.= (RealFuncAdd (Seg n)) . (x,y) by A2 ; :: thesis: verum
end;
then Euclid_add n = RealFuncAdd (Seg n) by A4, BINOP_1:2;
then A5: the addF of RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) = the addF of (RealVectSpace (Seg n)) by REAL_NS1:def 4
.= the addF of RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) by EUCLID:def 8 ;
for x being Element of REAL
for y being Element of REAL n holds (Euclid_mult n) . (x,y) = (RealFuncExtMult (Seg n)) . (x,y)
proof
let x be Element of REAL ; :: thesis: for y being Element of REAL n holds (Euclid_mult n) . (x,y) = (RealFuncExtMult (Seg n)) . (x,y)
let y be Element of REAL n; :: thesis: (Euclid_mult n) . (x,y) = (RealFuncExtMult (Seg n)) . (x,y)
reconsider y1 = y as Point of (TOP-REAL n) by A1, REAL_NS1:def 4;
reconsider x1 = x as Real ;
reconsider y2 = y as VECTOR of (REAL-NS n) by REAL_NS1:def 4;
thus (Euclid_mult n) . (x,y) = x1 * y2 by REAL_NS1:def 4
.= x1 * y1 by REAL_NS1:3
.= (RealFuncExtMult (Seg n)) . (x,y) by A2 ; :: thesis: verum
end;
then Euclid_mult n = RealFuncExtMult (Seg n) by A4, BINOP_1:2;
then the Mult of RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) = the Mult of (RealVectSpace (Seg n)) by REAL_NS1:def 4
.= the Mult of RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) by EUCLID:def 8 ;
hence RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) by A1, A3, A5; :: thesis: verum