set K = F_Complex ;
set qf = RQ*Form f;
set R = RKer (f *');
set qW = VectQuot (W,(RKer (f *')));
A1:
rightker f = rightker (f *')
by Th55;
thus
rightker (RQ*Form f) c= {(0. (VectQuot (W,(RKer (f *')))))}
XBOOLE_0:def 10,BILINEAR:def 24 K160( the carrier of (VectQuot (W,(RKer (f *')))),(0. (VectQuot (W,(RKer (f *')))))) c= rightker (RQ*Form f)proof
let x be
object ;
TARSKI:def 3 ( not x in rightker (RQ*Form f) or x in {(0. (VectQuot (W,(RKer (f *')))))} )
assume
x in rightker (RQ*Form f)
;
x in {(0. (VectQuot (W,(RKer (f *')))))}
then consider ww being
Vector of
(VectQuot (W,(RKer (f *')))) such that A2:
x = ww
and A3:
for
v being
Vector of
V holds
(RQ*Form f) . (
v,
ww)
= 0. F_Complex
;
consider w being
Vector of
W such that A4:
ww = w + (RKer (f *'))
by VECTSP10:22;
then
w in rightker f
;
then
w in the
carrier of
(RKer (f *'))
by A1, BILINEAR:def 19;
then
w in RKer (f *')
by STRUCT_0:def 5;
then w + (RKer (f *')) =
zeroCoset (
W,
(RKer (f *')))
by VECTSP_4:49
.=
0. (VectQuot (W,(RKer (f *'))))
by VECTSP10:21
;
hence
x in {(0. (VectQuot (W,(RKer (f *')))))}
by A2, A4, TARSKI:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in K160( the carrier of (VectQuot (W,(RKer (f *')))),(0. (VectQuot (W,(RKer (f *')))))) or x in rightker (RQ*Form f) )
assume
x in {(0. (VectQuot (W,(RKer (f *')))))}
; x in rightker (RQ*Form f)
then A5:
x = 0. (VectQuot (W,(RKer (f *'))))
by TARSKI:def 1;
for v being Vector of V holds (RQ*Form f) . (v,(0. (VectQuot (W,(RKer (f *')))))) = 0. F_Complex
by BILINEAR:29;
hence
x in rightker (RQ*Form f)
by A5; verum