let V be ComplexAlgebra; :: thesis: for V1 being ComplexSubAlgebra of V holds

( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

let V1 be ComplexSubAlgebra of V; :: thesis: ( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

let V1 be ComplexSubAlgebra of V; :: thesis: ( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

hereby :: thesis: ( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

let x1, y1 be Element of V1; :: thesis: for x, y being Element of V st x1 = x & y1 = y holds

x1 + y1 = x + y

let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 + y1 = x + y )

assume A1: ( x1 = x & y1 = y ) ; :: thesis: x1 + y1 = x + y

x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by Def1;

hence x1 + y1 = x + y by A1, FUNCT_1:49; :: thesis: verum

end;x1 + y1 = x + y

let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 + y1 = x + y )

assume A1: ( x1 = x & y1 = y ) ; :: thesis: x1 + y1 = x + y

x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by Def1;

hence x1 + y1 = x + y by A1, FUNCT_1:49; :: thesis: verum

hereby :: thesis: ( ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

let x1, y1 be Element of V1; :: thesis: for x, y being Element of V st x1 = x & y1 = y holds

x1 * y1 = x * y

let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 * y1 = x * y )

assume A2: ( x1 = x & y1 = y ) ; :: thesis: x1 * y1 = x * y

x1 * y1 = ( the multF of V || the carrier of V1) . [x1,y1] by Def1;

hence x1 * y1 = x * y by A2, FUNCT_1:49; :: thesis: verum

end;x1 * y1 = x * y

let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 * y1 = x * y )

assume A2: ( x1 = x & y1 = y ) ; :: thesis: x1 * y1 = x * y

x1 * y1 = ( the multF of V || the carrier of V1) . [x1,y1] by Def1;

hence x1 * y1 = x * y by A2, FUNCT_1:49; :: thesis: verum

hereby :: thesis: ( 1_ V1 = 1_ V & 0. V1 = 0. V )

thus
( 1_ V1 = 1_ V & 0. V1 = 0. V )
by Def1; :: thesis: verumlet v1 be Element of V1; :: thesis: for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v

let v be Element of V; :: thesis: for a being Complex st v1 = v holds

a * v1 = a * v

let a be Complex; :: thesis: ( v1 = v implies a * v1 = a * v )

assume A3: v1 = v ; :: thesis: a * v1 = a * v

reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

a1 * v1 = ( the Mult of V | [:COMPLEX, the carrier of V1:]) . [a1,v1] by Def1;

then a1 * v1 = a1 * v by A3, FUNCT_1:49;

hence a * v1 = a * v ; :: thesis: verum

end;for a being Complex st v1 = v holds

a * v1 = a * v

let v be Element of V; :: thesis: for a being Complex st v1 = v holds

a * v1 = a * v

let a be Complex; :: thesis: ( v1 = v implies a * v1 = a * v )

assume A3: v1 = v ; :: thesis: a * v1 = a * v

reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

a1 * v1 = ( the Mult of V | [:COMPLEX, the carrier of V1:]) . [a1,v1] by Def1;

then a1 * v1 = a1 * v by A3, FUNCT_1:49;

hence a * v1 = a * v ; :: thesis: verum