set A = the carrier of N;
set C = product <% the carrier of N, the carrier of N%>;
defpred S1[ Element of product <% the carrier of N, the carrier of N%>, Element of product <% the carrier of N, the carrier of N%>, set ] means ex a1, a2, b1, b2 being Element of N st
( $1 = <%a1,b1%> & $2 = <%a2,b2%> & $3 = <%(a1 + a2),(b1 + b2)%> );
A1: for x, y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S1[x,y,z]
proof
let a, b be Element of product <% the carrier of N, the carrier of N%>; :: thesis: ex z being Element of product <% the carrier of N, the carrier of N%> st S1[a,b,z]
consider a1, b1 being set such that
A2: ( a1 in the carrier of N & b1 in the carrier of N ) and
A3: a = <%a1,b1%> by Th7;
consider a2, b2 being set such that
A4: ( a2 in the carrier of N & b2 in the carrier of N ) and
A5: b = <%a2,b2%> by Th7;
reconsider a1 = a1, a2 = a2, b1 = b1, b2 = b2 as Element of the carrier of N by A2, A4;
take c = <%(a1 + a2),(b1 + b2)%>; :: thesis: ( c is Element of product <% the carrier of N, the carrier of N%> & S1[a,b,c] )
thus c is Element of product <% the carrier of N, the carrier of N%> by Th6; :: thesis: S1[a,b,c]
thus S1[a,b,c] by A3, A5; :: thesis: verum
end;
consider add being Function of [:(product <% the carrier of N, the carrier of N%>),(product <% the carrier of N, the carrier of N%>):],(product <% the carrier of N, the carrier of N%>) such that
A6: for x, y being Element of product <% the carrier of N, the carrier of N%> holds S1[x,y,add . (x,y)] from BINOP_1:sch 3(A1);
 defpred S2[ Element of product <% the carrier of N, the carrier of N%>, Element of product <% the carrier of N, the carrier of N%>, set ] means ex a1, a2, b1, b2 being Element of N st
( $1 = <%a1,b1%> & $2 = <%a2,b2%> & $3 = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> );
A7: for x, y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S2[x,y,z]
proof
let a, b be Element of product <% the carrier of N, the carrier of N%>; :: thesis: ex z being Element of product <% the carrier of N, the carrier of N%> st S2[a,b,z]
consider a1, b1 being set such that
A8: ( a1 in the carrier of N & b1 in the carrier of N ) and
A9: a = <%a1,b1%> by Th7;
consider a2, b2 being set such that
A10: ( a2 in the carrier of N & b2 in the carrier of N ) and
A11: b = <%a2,b2%> by Th7;
reconsider a1 = a1, a2 = a2, b1 = b1, b2 = b2 as Element of the carrier of N by A8, A10;
take z = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%>; :: thesis: ( z is Element of product <% the carrier of N, the carrier of N%> & S2[a,b,z] )
thus z is Element of product <% the carrier of N, the carrier of N%> by Th6; :: thesis: S2[a,b,z]
thus S2[a,b,z] by A9, A11; :: thesis: verum
end;
consider mult being Function of [:(product <% the carrier of N, the carrier of N%>),(product <% the carrier of N, the carrier of N%>):],(product <% the carrier of N, the carrier of N%>) such that
A12: for x, y being Element of product <% the carrier of N, the carrier of N%> holds S2[x,y,mult . (x,y)] from BINOP_1:sch 3(A7);
 defpred S3[ Element of REAL , Element of product <% the carrier of N, the carrier of N%>, set ] means ex a, b being Element of N st
( $2 = <%a,b%> & $3 = <%($1 * a),($1 * b)%> );
A13: for x being Element of REAL
for y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S3[x,y,z]
proof
let r be Element of REAL ; :: thesis: for y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S3[r,y,z]
let c be Element of product <% the carrier of N, the carrier of N%>; :: thesis: ex z being Element of product <% the carrier of N, the carrier of N%> st S3[r,c,z]
consider a, b being set such that
A14: ( a in the carrier of N & b in the carrier of N ) and
A15: c = <%a,b%> by Th7;
reconsider a = a, b = b as Element of the carrier of N by A14;
take z = <%(r * a),(r * b)%>; :: thesis: ( z is Element of product <% the carrier of N, the carrier of N%> & S3[r,c,z] )
thus z is Element of product <% the carrier of N, the carrier of N%> by Th6; :: thesis: S3[r,c,z]
thus S3[r,c,z] by A15; :: thesis: verum
end;
consider MU being Function of [:REAL,(product <% the carrier of N, the carrier of N%>):],(product <% the carrier of N, the carrier of N%>) such that
A16: for x being Element of REAL
for y being Element of product <% the carrier of N, the carrier of N%> holds S3[x,y,MU . (x,y)] from BINOP_1:sch 3(A13);
 defpred S4[ Element of product <% the carrier of N, the carrier of N%>, set ] means ex a, b being Element of N st
( $1 = <%a,b%> & $2 = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) );
A17: for x being Element of product <% the carrier of N, the carrier of N%> ex y being Element of REAL st S4[x,y]
proof
let c be Element of product <% the carrier of N, the carrier of N%>; :: thesis: ex y being Element of REAL st S4[c,y]
consider a, b being set such that
A18: ( a in the carrier of N & b in the carrier of N ) and
A19: c = <%a,b%> by Th7;
reconsider a = a, b = b as Element of the carrier of N by A18;
take sqrt ((||.a.|| ^2) + (||.b.|| ^2)) ; :: thesis: ( sqrt ((||.a.|| ^2) + (||.b.|| ^2)) is set & sqrt ((||.a.|| ^2) + (||.b.|| ^2)) is Element of REAL & S4[c, sqrt ((||.a.|| ^2) + (||.b.|| ^2))] )
thus ( sqrt ((||.a.|| ^2) + (||.b.|| ^2)) is set & sqrt ((||.a.|| ^2) + (||.b.|| ^2)) is Element of REAL & S4[c, sqrt ((||.a.|| ^2) + (||.b.|| ^2))] ) by A19, XREAL_0:def 1, TARSKI:1; :: thesis: verum
end;
consider norm being Function of (product <% the carrier of N, the carrier of N%>),REAL such that
A20: for x being Element of product <% the carrier of N, the carrier of N%> holds S4[x,norm . x] from FUNCT_2:sch 3(A17);
 defpred S5[ Element of product <% the carrier of N, the carrier of N%>, set ] means ex a, b being Element of N st
( $1 = <%a,b%> & $2 = <%(a *'),(- b)%> );
A21: for x being Element of product <% the carrier of N, the carrier of N%> ex y being Element of product <% the carrier of N, the carrier of N%> st S5[x,y]
proof
let c be Element of product <% the carrier of N, the carrier of N%>; :: thesis: ex y being Element of product <% the carrier of N, the carrier of N%> st S5[c,y]
consider a, b being set such that
A22: ( a in the carrier of N & b in the carrier of N ) and
A23: c = <%a,b%> by Th7;
reconsider a = a, b = b as Element of the carrier of N by A22;
take <%(a *'),(- b)%> ; :: thesis: ( <%(a *'),(- b)%> is Element of product <% the carrier of N, the carrier of N%> & S5[c,<%(a *'),(- b)%>] )
thus ( <%(a *'),(- b)%> is Element of product <% the carrier of N, the carrier of N%> & S5[c,<%(a *'),(- b)%>] ) by A23, Th6; :: thesis: verum
end;
consider conj being Function of (product <% the carrier of N, the carrier of N%>),(product <% the carrier of N, the carrier of N%>) such that
A24: for x being Element of product <% the carrier of N, the carrier of N%> holds S5[x,conj . x] from FUNCT_2:sch 3(A21);
 reconsider Z = <%(0. N),(0. N)%>, O = <%(1. N),(0. N)%> as Element of product <% the carrier of N, the carrier of N%> by Th6;
take X = ConjNormAlgStr(# (product <% the carrier of N, the carrier of N%>),mult,add,MU,O,Z,norm,conj #); :: thesis: ( the carrier of X = product <% the carrier of N, the carrier of N%> & the ZeroF of X = <%(0. N),(0. N)%> & the OneF of X = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of X . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> ) ) )
thus ( the carrier of X = product <% the carrier of N, the carrier of N%> & the ZeroF of X = <%(0. N),(0. N)%> & the OneF of X = <%(1. N),(0. N)%> ) ; :: thesis: ( ( for a1, a2, b1, b2 being Element of N holds
( the addF of X . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> ) ) )
hereby :: thesis: ( ( for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> ) ) )
let a1, a2, b1, b2 be Element of N; :: thesis: ( the addF of X . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> )
reconsider a = <%a1,b1%>, b = <%a2,b2%> as Element of product <% the carrier of N, the carrier of N%> by Th6;
consider x1, x2, y1, y2 being Element of N such that
A25: ( a = <%x1,y1%> & b = <%x2,y2%> ) and
A26: add . (a,b) = <%(x1 + x2),(y1 + y2)%> by A6;
( a1 = x1 & a2 = x2 & b1 = y1 & b2 = y2 ) by A25, Th3;
hence the addF of X . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> by A26; :: thesis: the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%>
consider x1, x2, y1, y2 being Element of N such that
A27: ( a = <%x1,y1%> & b = <%x2,y2%> ) and
A28: mult . (a,b) = <%((x1 * x2) - ((y2 *') * y1)),((y2 * x1) + (y1 * (x2 *')))%> by A12;
( a1 = x1 & a2 = x2 & b1 = y1 & b2 = y2 ) by A27, Th3;
hence the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> by A28; :: thesis: verum
end;
hereby :: thesis: for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> )
let r be Real; :: thesis: for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%>
let a, b be Element of N; :: thesis: the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%>
reconsider c = <%a,b%> as Element of product <% the carrier of N, the carrier of N%> by Th6;
r in REAL by XREAL_0:def 1;
then consider x, y being Element of N such that
A29: c = <%x,y%> and
A30: MU . (r,c) = <%(r * x),(r * y)%> by A16;
( a = x & b = y ) by A29, Th3;
hence the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> by A30; :: thesis: verum
end;
hereby :: thesis: verum
let a, b be Element of N; :: thesis: ( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> )
reconsider c = <%a,b%> as Element of product <% the carrier of N, the carrier of N%> by Th6;
consider x, y being Element of N such that
A31: c = <%x,y%> and
A32: norm . c = sqrt ((||.x.|| ^2) + (||.y.|| ^2)) by A20;
( a = x & b = y ) by A31, Th3;
hence the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) by A32; :: thesis: the conjugateF of X . <%a,b%> = <%(a *'),(- b)%>
consider x, y being Element of N such that
A33: c = <%x,y%> and
A34: conj . c = <%(x *'),(- y)%> by A24;
( a = x & b = y ) by A33, Th3;
hence the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> by A34; :: thesis: verum
end;