begin
deffunc H1( UNITSTR ) -> Element of the carrier of $1 = 0. $1;
set V0 = the RealLinearSpace;
Lm1:
the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}
by RLSUB_1:def 3;
reconsider nilfunc = [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):] --> 0 as Function of [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):],REAL by FUNCOP_1:45;
( ( for x, y being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [x,y] = 0 ) & 0. the RealLinearSpace in the carrier of ((0). the RealLinearSpace) )
by Lm1, FUNCOP_1:7, TARSKI:def 1;
then Lm2:
nilfunc . [(0. the RealLinearSpace),(0. the RealLinearSpace)] = 0
;
Lm3:
for u, v being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [u,v] = nilfunc . [v,u]
Lm4:
for u, v, w being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm5:
for u, v being VECTOR of ((0). the RealLinearSpace)
for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
set X0 = UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #);
Lm6:
now for x, y, z being Point of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)
for a being Real holds
( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let x,
y,
z be
Point of
UNITSTR(# the
carrier of
((0). the RealLinearSpace),
(0. ((0). the RealLinearSpace)), the
addF of
((0). the RealLinearSpace), the
Mult of
((0). the RealLinearSpace),
nilfunc #);
for a being Real holds
( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )let a be
Real;
( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
H1(
UNITSTR(# the
carrier of
((0). the RealLinearSpace),
(0. ((0). the RealLinearSpace)), the
addF of
((0). the RealLinearSpace), the
Mult of
((0). the RealLinearSpace),
nilfunc #))
= 0. the
RealLinearSpace
by RLSUB_1:11;
hence
(
x .|. x = 0 iff
x = H1(
UNITSTR(# the
carrier of
((0). the RealLinearSpace),
(0. ((0). the RealLinearSpace)), the
addF of
((0). the RealLinearSpace), the
Mult of
((0). the RealLinearSpace),
nilfunc #)) )
by Lm1, FUNCOP_1:7, TARSKI:def 1;
( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
0 <= x .|. x
by FUNCOP_1:7;
( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
x .|. y = y .|. x
by Lm3;
( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(x + y) .|. z = (x .|. z) + (y .|. z)
(a * x) .|. y = a * (x .|. y)
thus
(a * x) .|. y = a * (x .|. y)
verum
end;