let L be INTegral Z_Lattice; :: thesis: InnerProduct L is bilinear-Form of L,L
X1: dom (InnerProduct L) = [: the carrier of L, the carrier of L:] by FUNCT_2:def 1;
for z being object st z in [: the carrier of L, the carrier of L:] holds
(InnerProduct L) . z in the carrier of INT.Ring

proof

let z be object ; :: thesis: ( z in [: the carrier of L, the carrier of L:] implies (InnerProduct L) . z in the carrier of INT.Ring )
assume z in [: the carrier of L, the carrier of L:] ; :: thesis: (InnerProduct L) . z in the carrier of INT.Ring
then consider x1, x2 being object such that
B1: ( x1 in the carrier of L & x2 in the carrier of L & z = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Vector of L by B1;
(InnerProduct L) . z = <;x1,x2;> by B1;
hence (InnerProduct L) . z in the carrier of INT.Ring by defIntegral; :: thesis: verum

end;

then reconsider f = InnerProduct L as Form of L,L by X1, FUNCT_2:3;
for v being Vector of L holds FunctionalSAF (f,v) is additive

proof

let v be Vector of L; :: thesis: FunctionalSAF (f,v) is additive
for x, y being Vector of L holds (FunctionalSAF (f,v)) . (x + y) = ((FunctionalSAF (f,v)) . x) + ((FunctionalSAF (f,v)) . y)

proof

let x, y be Vector of L; :: thesis: (FunctionalSAF (f,v)) . (x + y) = ((FunctionalSAF (f,v)) . x) + ((FunctionalSAF (f,v)) . y)
thus (FunctionalSAF (f,v)) . (x + y) = f . ((x + y),v) by FUNCT_5:70
.= <;(x + y),v;>
.= <;v,(x + y);> by defZLattice
.= <;v,x;> + <;v,y;> by ThSc2
.= <;x,v;> + <;v,y;> by defZLattice
.= <;x,v;> + <;y,v;> by defZLattice
.= (f . (x,v)) + (f . (y,v))
.= (((curry' f) . v) . x) + (f . (y,v)) by FUNCT_5:70
.= ((FunctionalSAF (f,v)) . x) + ((FunctionalSAF (f,v)) . y) by FUNCT_5:70 ; :: thesis: verum

end;

hence FunctionalSAF (f,v) is additive ; :: thesis: verum

end;

then X1: f is additiveSAF ;
for v being Vector of L holds FunctionalSAF (f,v) is homogeneous

proof

let v be Vector of L; :: thesis: FunctionalSAF (f,v) is homogeneous
for x being Vector of L
for i being Element of INT.Ring holds (FunctionalSAF (f,v)) . (i * x) = i * ((FunctionalSAF (f,v)) . x)

proof

let x be Vector of L; :: thesis: for i being Element of INT.Ring holds (FunctionalSAF (f,v)) . (i * x) = i * ((FunctionalSAF (f,v)) . x)
let i be Element of INT.Ring; :: thesis: (FunctionalSAF (f,v)) . (i * x) = i * ((FunctionalSAF (f,v)) . x)
thus (FunctionalSAF (f,v)) . (i * x) = f . ((i * x),v) by FUNCT_5:70
.= <;(i * x),v;>
.= <;v,(i * x);> by defZLattice
.= i * <;v,x;> by ThSc3
.= i * <;x,v;> by defZLattice
.= i * (f . (x,v))
.= i * ((FunctionalSAF (f,v)) . x) by FUNCT_5:70 ; :: thesis: verum

end;

hence FunctionalSAF (f,v) is homogeneous ; :: thesis: verum

end;

then X2: f is homogeneousSAF ;
for v being Vector of L holds FunctionalFAF (f,v) is additive

proof

let v be Vector of L; :: thesis: FunctionalFAF (f,v) is additive
for x, y being Vector of L holds (FunctionalFAF (f,v)) . (x + y) = ((FunctionalFAF (f,v)) . x) + ((FunctionalFAF (f,v)) . y)

proof

let x, y be Vector of L; :: thesis: (FunctionalFAF (f,v)) . (x + y) = ((FunctionalFAF (f,v)) . x) + ((FunctionalFAF (f,v)) . y)
thus (FunctionalFAF (f,v)) . (x + y) = f . (v,(x + y)) by FUNCT_5:69
.= <;v,(x + y);>
.= <;v,x;> + <;v,y;> by ThSc2
.= (f . (v,x)) + (f . (v,y))
.= (((curry f) . v) . x) + (f . (v,y)) by FUNCT_5:69
.= ((FunctionalFAF (f,v)) . x) + ((FunctionalFAF (f,v)) . y) by FUNCT_5:69 ; :: thesis: verum

end;

hence FunctionalFAF (f,v) is additive ; :: thesis: verum

end;

then X3: f is additiveFAF ;
for v being Vector of L holds FunctionalFAF (f,v) is homogeneous

proof

let v be Vector of L; :: thesis: FunctionalFAF (f,v) is homogeneous
for x being Vector of L
for i being Element of INT.Ring holds (FunctionalFAF (f,v)) . (i * x) = i * ((FunctionalFAF (f,v)) . x)

proof

let x be Vector of L; :: thesis: for i being Element of INT.Ring holds (FunctionalFAF (f,v)) . (i * x) = i * ((FunctionalFAF (f,v)) . x)
let i be Element of INT.Ring; :: thesis: (FunctionalFAF (f,v)) . (i * x) = i * ((FunctionalFAF (f,v)) . x)
thus (FunctionalFAF (f,v)) . (i * x) = f . (v,(i * x)) by FUNCT_5:69
.= <;v,(i * x);>
.= i * <;v,x;> by ThSc3
.= i * (f . (v,x))
.= i * ((FunctionalFAF (f,v)) . x) by FUNCT_5:69 ; :: thesis: verum

end;

hence FunctionalFAF (f,v) is homogeneous ; :: thesis: verum

end;

then f is homogeneousFAF ;
hence InnerProduct L is bilinear-Form of L,L by X1, X2, X3; :: thesis: verum