let X, Y be strict ConjNormAlgStr ; ( 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)%> ) ) & the carrier of Y = product <% the carrier of N, the carrier of N%> & the ZeroF of Y = <%(0. N),(0. N)%> & the OneF of Y = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of Y . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of Y . (<%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 Y . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of Y . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of Y . <%a,b%> = <%(a *'),(- b)%> ) ) implies X = Y )
assume that
A35:
the carrier of X = product <% the carrier of N, the carrier of N%>
and
A36:
the ZeroF of X = <%(0. N),(0. N)%>
and
A37:
the OneF of X = <%(1. N),(0. N)%>
and
A38:
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 *')))%> )
and
A39:
for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%>
and
A40:
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)%> )
and
A41:
the carrier of Y = product <% the carrier of N, the carrier of N%>
and
A42:
the ZeroF of Y = <%(0. N),(0. N)%>
and
A43:
the OneF of Y = <%(1. N),(0. N)%>
and
A44:
for a1, a2, b1, b2 being Element of N holds
( the addF of Y . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of Y . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> )
and
A45:
for r being Real
for a, b being Element of N holds the Mult of Y . (r,<%a,b%>) = <%(r * a),(r * b)%>
and
A46:
for a, b being Element of N holds
( the normF of Y . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of Y . <%a,b%> = <%(a *'),(- b)%> )
; X = Y
A47:
the addF of X = the addF of Y
proof
dom the
addF of
X = [: the carrier of X, the carrier of X:]
by A35, FUNCT_2:def 1;
hence
dom the
addF of
X = dom the
addF of
Y
by A35, A41, FUNCT_2:def 1;
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom the addF of X or the addF of X . b1 = the addF of Y . b1 )
let z be
object ;
( not z in dom the addF of X or the addF of X . z = the addF of Y . z )
assume
z in dom the
addF of
X
;
the addF of X . z = the addF of Y . z
then consider z1,
z2 being
object such that A48:
z1 in the
carrier of
X
and A49:
z2 in the
carrier of
X
and A50:
z = [z1,z2]
by ZFMISC_1:def 2;
consider a1,
b1 being
set such that A51:
(
a1 in the
carrier of
N &
b1 in the
carrier of
N )
and A52:
z1 = <%a1,b1%>
by A35, A48, Th7;
consider a2,
b2 being
set such that A53:
(
a2 in the
carrier of
N &
b2 in the
carrier of
N )
and A54:
z2 = <%a2,b2%>
by A35, A49, Th7;
reconsider a1 =
a1,
a2 =
a2,
b1 =
b1,
b2 =
b2 as
Element of
N by A51, A53;
thus the
addF of
X . z =
the
addF of
X . (
z1,
z2)
by A50
.=
<%(a1 + a2),(b1 + b2)%>
by A52, A54, A38
.=
the
addF of
Y . (
z1,
z2)
by A52, A54, A44
.=
the
addF of
Y . z
by A50
;
verum
end;
A55:
the multF of X = the multF of Y
proof
dom the
multF of
X = [: the carrier of X, the carrier of X:]
by A35, FUNCT_2:def 1;
hence
dom the
multF of
X = dom the
multF of
Y
by A35, A41, FUNCT_2:def 1;
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom the multF of X or the multF of X . b1 = the multF of Y . b1 )
let z be
object ;
( not z in dom the multF of X or the multF of X . z = the multF of Y . z )
assume
z in dom the
multF of
X
;
the multF of X . z = the multF of Y . z
then consider z1,
z2 being
object such that A56:
z1 in the
carrier of
X
and A57:
z2 in the
carrier of
X
and A58:
z = [z1,z2]
by ZFMISC_1:def 2;
consider a1,
b1 being
set such that A59:
(
a1 in the
carrier of
N &
b1 in the
carrier of
N )
and A60:
z1 = <%a1,b1%>
by A35, A56, Th7;
consider a2,
b2 being
set such that A61:
(
a2 in the
carrier of
N &
b2 in the
carrier of
N )
and A62:
z2 = <%a2,b2%>
by A35, A57, Th7;
reconsider a1 =
a1,
a2 =
a2,
b1 =
b1,
b2 =
b2 as
Element of
N by A59, A61;
thus the
multF of
X . z =
the
multF of
X . (
z1,
z2)
by A58
.=
<%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%>
by A60, A62, A38
.=
the
multF of
Y . (
z1,
z2)
by A60, A62, A44
.=
the
multF of
Y . z
by A58
;
verum
end;
A63:
the Mult of X = the Mult of Y
proof
dom the
Mult of
X = [:REAL, the carrier of X:]
by A35, FUNCT_2:def 1;
hence
dom the
Mult of
X = dom the
Mult of
Y
by A35, A41, FUNCT_2:def 1;
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom the Mult of X or the Mult of X . b1 = the Mult of Y . b1 )
let z be
object ;
( not z in dom the Mult of X or the Mult of X . z = the Mult of Y . z )
assume
z in dom the
Mult of
X
;
the Mult of X . z = the Mult of Y . z
then consider z1,
z2 being
object such that A64:
z1 in REAL
and A65:
z2 in the
carrier of
X
and A66:
z = [z1,z2]
by ZFMISC_1:def 2;
consider a,
b being
set such that A67:
(
a in the
carrier of
N &
b in the
carrier of
N )
and A68:
z2 = <%a,b%>
by A35, A65, Th7;
reconsider z1 =
z1 as
Element of
REAL by A64;
reconsider a =
a,
b =
b as
Element of
N by A67;
thus the
Mult of
X . z =
the
Mult of
X . (
z1,
z2)
by A66
.=
<%(z1 * a),(z1 * b)%>
by A68, A39
.=
the
Mult of
Y . (
z1,
z2)
by A68, A45
.=
the
Mult of
Y . z
by A66
;
verum
end;
A69:
the normF of X = the normF of Y
the conjugateF of X = the conjugateF of Y
proof
dom the
conjugateF of
X = the
carrier of
X
by A35, FUNCT_2:def 1;
hence
dom the
conjugateF of
X = dom the
conjugateF of
Y
by A35, A41, FUNCT_2:def 1;
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom the conjugateF of X or the conjugateF of X . b1 = the conjugateF of Y . b1 )
let z be
object ;
( not z in dom the conjugateF of X or the conjugateF of X . z = the conjugateF of Y . z )
assume
z in dom the
conjugateF of
X
;
the conjugateF of X . z = the conjugateF of Y . z
then consider a,
b being
set such that A72:
(
a in the
carrier of
N &
b in the
carrier of
N )
and A73:
z = <%a,b%>
by A35, Th7;
reconsider a =
a,
b =
b as
Element of
N by A72;
thus the
conjugateF of
X . z =
<%(a *'),(- b)%>
by A73, A40
.=
the
conjugateF of
Y . z
by A73, A46
;
verum
end;
hence
X = Y
by A35, A36, A37, A41, A42, A43, A47, A55, A63, A69; verum