let V be Algebra; :: thesis: for V1 being Subalgebra 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 Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let V1 be Subalgebra 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 Real 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 Real 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 AS: ( x1 = x & y1 = y ) ; :: thesis: x1 + y1 = x + y
x1 + y1 = (the addF of V || the carrier of V1) . [x1,y1] by DefSubAlg;
hence x1 + y1 = x + y by AS, FUNCT_1:72; :: thesis: verum

end;

hereby :: thesis: ( ( for v1 being Element of V1
for v being Element of V
for a being Real 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 AS: ( x1 = x & y1 = y ) ; :: thesis: x1 * y1 = x * y
x1 * y1 = (the multF of V || the carrier of V1) . [x1,y1] by DefSubAlg;
hence x1 * y1 = x * y by AS, FUNCT_1:72; :: thesis: verum

end;

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

let v1 be Element of V1; :: thesis: for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v
let v be Element of V; :: thesis: for a being Real st v1 = v holds
a * v1 = a * v
let a be Real; :: thesis: ( v1 = v implies a * v1 = a * v )
assume AS: v1 = v ; :: thesis: a * v1 = a * v
a * v1 = (the Mult of V | [:REAL ,the carrier of V1:]) . [a,v1] by DefSubAlg;
hence a * v1 = a * v by AS, FUNCT_1:72; :: thesis: verum

end;

thus ( 1_ V1 = 1_ V & 0. V1 = 0. V ) by DefSubAlg; :: thesis: verum