let f1, f2 be Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)); :: thesis: ( ( for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & f1 . x = Dir v ) ) & ( for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & f2 . x = Dir v ) ) implies f1 = f2 )
assume that
A9: for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & f1 . x = Dir v ) and
A10: for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & f2 . x = Dir v ) ; :: thesis: f1 = f2
now :: thesis: ( dom f1 = dom f2 & ( for x being object st x in dom f1 holds
f1 . x = f2 . x ) )
reconsider g1 = f1 as Function of the carrier of (ProjectiveSpace (TOP-REAL 3)), the carrier of (ProjectiveSpace (TOP-REAL 3)) ;
dom g1 = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence dom f1 = dom f2 by FUNCT_2:def 1; :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x
hereby :: thesis: verum
let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A11: x in dom f1 ; :: thesis: f1 . x = f2 . x
then consider u1, v1 being Element of (TOP-REAL 3), uf1 being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that
A12: x = Dir u1 and
A13: not u1 is zero and
A14: u1 = uf1 and
A15: p1 = N * uf1 and
A16: v1 = M2F p1 and
not v1 is zero and
A17: f1 . x = Dir v1 by A9;
consider u2, v2 being Element of (TOP-REAL 3), uf2 being FinSequence of F_Real, p2 being FinSequence of 1 -tuples_on REAL such that
A18: x = Dir u2 and
A19: not u2 is zero and
A20: u2 = uf2 and
A21: p2 = N * uf2 and
A22: v2 = M2F p2 and
not v2 is zero and
A23: f2 . x = Dir v2 by A11, A10;
are_Prop u1,u2 by A12, A13, A18, A19, ANPROJ_1:22;
then consider a being Real such that
A24: a <> 0 and
A25: u1 = a * u2 by ANPROJ_1:1;
B01: width N = 3 by MATRIX_0:23;
A26: now :: thesis: len (<*uf1*> @) = 3
len uf1 = 3 by A14, FINSEQ_3:153;
then width <*uf1*> = 3 by Th61;
hence len (<*uf1*> @) = width <*uf1*> by MATRIX_0:29
.= len uf1 by MATRIX_0:23
.= 3 by A14, FINSEQ_3:153 ;
:: thesis: verum
end;
A27: now :: thesis: len (<*uf2*> @) = 3
len uf2 = 3 by A20, FINSEQ_3:153;
then width <*uf2*> = 3 by Th61;
hence len (<*uf2*> @) = width <*uf2*> by MATRIX_0:29
.= len uf2 by MATRIX_0:23
.= 3 by A20, FINSEQ_3:153 ;
:: thesis: verum
end;
A28: len p2 = len (N * (<*uf2*> @)) by A21, LAPLACE:def 9
.= len N by B01, A27, MATRIX_3:def 4 ;
now :: thesis: ( v1 = a * v2 & not v1 is zero & not v2 is zero )
M2F p1 = a * v2
proof
len p2 = 3 by A28, MATRIX_0:23;
then consider q1, q2, q3 being Real such that
A29: ( q1 = (p2 . 1) . 1 & q2 = (p2 . 2) . 1 & q3 = (p2 . 3) . 1 ) and
A30: a * p2 = <*<*(a * q1)*>,<*(a * q2)*>,<*(a * q3)*>*> by DEF3;
A31: len (a * p2) = 3 by A30, FINSEQ_1:45;
A32: N * (<*uf1*> @) is Matrix of 3,1,F_Real by A14, FINSEQ_3:153, Th74;
then A33: Indices (N * (<*uf1*> @)) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
A34: N * (<*uf2*> @) is 3,1 -size by A20, FINSEQ_3:153, Th74;
A35: len p1 = len (N * (<*uf1*> @)) by A15, LAPLACE:def 9
.= 3 by A32, MATRIX_0:23 ;
A36: p1 = a * p2
proof
p1 = <*<*(a * q1)*>,<*(a * q2)*>,<*(a * q3)*>*>
proof
A37: p1 = N * (<*uf1*> @) by A15, LAPLACE:def 9;
then A38: len p1 = len N by B01, A26, MATRIX_3:def 4
.= 3 by MATRIX_0:23 ;
A39: p2 = N * (<*uf2*> @) by A21, LAPLACE:def 9;
A40: N * (<*uf1*> @) is Matrix of 3,1,F_Real by A14, FINSEQ_3:153, Th74;
A41: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
A42: Seg (width (N * (<*uf1*> @))) = Seg 1 by A32, MATRIX_0:23;
A43: N * (<*uf2*> @) is Matrix of 3,1,F_Real by A20, FINSEQ_3:153, Th74;
A44: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
A45: Seg (width (N * (<*uf2*> @))) = Seg 1 by A43, MATRIX_0:23;
now :: thesis: ( len p1 = 3 & p1 . 1 = <*(a * q1)*> & p1 . 2 = <*(a * q2)*> & p1 . 3 = <*(a * q3)*> )
thus len p1 = 3 by A38; :: thesis: ( p1 . 1 = <*(a * q1)*> & p1 . 2 = <*(a * q2)*> & p1 . 3 = <*(a * q3)*> )
thus p1 . 1 = <*(a * q1)*> :: thesis: ( p1 . 2 = <*(a * q2)*> & p1 . 3 = <*(a * q3)*> )
proof
A46: [1,1] in Indices (N * (<*uf2*> @)) by Th2, A34, MATRIX_0:23;
A47: p1 . 1 = Line ((N * (<*uf1*> @)),1) by A37, A40, A41, MATRIX_0:52;
then A48: len (p1 . 1) = width (N * (<*uf1*> @)) by MATRIX_0:def 7
.= 1 by A40, MATRIX_0:23 ;
A49: (p1 . 1) . 1 = (N * (<*uf1*> @)) * (1,1) by A47, FINSEQ_1:1, A42, MATRIX_0:def 7
.= (Line (N,1)) "*" (Col ((<*uf1*> @),1)) by B01, A26, Th2, A33, MATRIX_3:def 4 ;
A50: p2 . 1 = Line ((N * (<*uf2*> @)),1) by A39, A43, A44, MATRIX_0:52;
A51: (p2 . 1) . 1 = (N * (<*uf2*> @)) * (1,1) by A50, FINSEQ_1:1, A45, MATRIX_0:def 7
.= (Line (N,1)) "*" (Col ((<*uf2*> @),1)) by B01, A46, A27, MATRIX_3:def 4 ;
(Line (N,1)) "*" (Col ((<*uf1*> @),1)) = a * ((Line (N,1)) "*" (Col ((<*uf2*> @),1)))
proof
A52: ( u1 `1 = u1 . 1 & u1 `2 = u1 . 2 & u1 `3 = u1 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
A53: u1 = |[(u1 . 1),(u1 . 2),(u1 . 3)]| by A52, EUCLID_5:3;
( u2 `1 = u2 . 1 & u2 `2 = u2 . 2 & u2 `3 = u2 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A54: u2 = |[(u2 . 1),(u2 . 2),(u2 . 3)]| by EUCLID_5:3;
A55: u1 = |[(a * (u2 . 1)),(a * (u2 . 2)),(a * (u2 . 3))]| by A25, A54, EUCLID_5:8;
A56: ( Col ((<*uf1*> @),1) = u1 & Col ((<*uf2*> @),1) = u2 ) by Th76, A14, A20;
A57: len (Line (N,1)) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ;
now :: thesis: ( len (Line (N,1)) = 3 & (Line (N,1)) . 1 = N * (1,1) & (Line (N,1)) . 2 = N * (1,2) & (Line (N,1)) . 3 = N * (1,3) )
thus len (Line (N,1)) = 3 by A57; :: thesis: ( (Line (N,1)) . 1 = N * (1,1) & (Line (N,1)) . 2 = N * (1,2) & (Line (N,1)) . 3 = N * (1,3) )
Seg (width N) = Seg 3 by MATRIX_0:23;
hence ( (Line (N,1)) . 1 = N * (1,1) & (Line (N,1)) . 2 = N * (1,2) & (Line (N,1)) . 3 = N * (1,3) ) by FINSEQ_1:1, MATRIX_0:def 7; :: thesis: verum
end;
then A58: Line (N,1) = <*(N * (1,1)),(N * (1,2)),(N * (1,3))*> by FINSEQ_1:45;
reconsider z1 = u1 . 1, z2 = u1 . 2, z3 = u1 . 3, z4 = u2 . 1, z5 = u2 . 2, z6 = u2 . 3 as Element of F_Real by XREAL_0:def 1;
A59: (Line (N,1)) "*" (Col ((<*uf1*> @),1)) = (((N * (1,1)) * z1) + ((N * (1,2)) * z2)) + ((N * (1,3)) * z3) by A58, A53, A56, Th6;
A60: (Line (N,1)) "*" (Col ((<*uf2*> @),1)) = (((N * (1,1)) * z4) + ((N * (1,2)) * z5)) + ((N * (1,3)) * z6) by A54, A58, A56, Th6;
( u1 . 1 = a * (u2 . 1) & u1 . 2 = a * (u2 . 2) & u1 . 3 = a * (u2 . 3) ) by A55, A53, FINSEQ_1:78;
hence (Line (N,1)) "*" (Col ((<*uf1*> @),1)) = a * ((Line (N,1)) "*" (Col ((<*uf2*> @),1))) by A59, A60; :: thesis: verum
end;
hence p1 . 1 = <*(a * q1)*> by A29, A51, A48, FINSEQ_1:40, A49; :: thesis: verum
end;
thus p1 . 2 = <*(a * q2)*> :: thesis: p1 . 3 = <*(a * q3)*>
proof
A61: [2,1] in Indices (N * (<*uf2*> @)) by Th2, A34, MATRIX_0:23;
A62: [2,1] in Indices (N * (<*uf1*> @)) by Th2, A32, MATRIX_0:23;
A63: p1 . 2 = Line ((N * (<*uf1*> @)),2) by A37, A40, A41, MATRIX_0:52;
then A64: len (p1 . 2) = width (N * (<*uf1*> @)) by MATRIX_0:def 7
.= 1 by A40, MATRIX_0:23 ;
A65: (p1 . 2) . 1 = (N * (<*uf1*> @)) * (2,1) by A63, FINSEQ_1:1, A42, MATRIX_0:def 7
.= (Line (N,2)) "*" (Col ((<*uf1*> @),1)) by B01, A26, A62, MATRIX_3:def 4 ;
p2 . 2 = Line ((N * (<*uf2*> @)),2) by A39, A43, A44, MATRIX_0:52;
then A66: (p2 . 2) . 1 = (N * (<*uf2*> @)) * (2,1) by FINSEQ_1:1, A45, MATRIX_0:def 7
.= (Line (N,2)) "*" (Col ((<*uf2*> @),1)) by B01, A27, A61, MATRIX_3:def 4 ;
(Line (N,2)) "*" (Col ((<*uf1*> @),1)) = a * ((Line (N,2)) "*" (Col ((<*uf2*> @),1)))
proof
( u1 `1 = u1 . 1 & u1 `2 = u1 . 2 & u1 `3 = u1 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A67: u1 = |[(u1 . 1),(u1 . 2),(u1 . 3)]| by EUCLID_5:3;
( u2 `1 = u2 . 1 & u2 `2 = u2 . 2 & u2 `3 = u2 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A68: u2 = |[(u2 . 1),(u2 . 2),(u2 . 3)]| by EUCLID_5:3;
then A69: u1 = |[(a * (u2 . 1)),(a * (u2 . 2)),(a * (u2 . 3))]| by A25, EUCLID_5:8;
A70: ( Col ((<*uf1*> @),1) = u1 & Col ((<*uf2*> @),1) = u2 ) by Th76, A14, A20;
A71: len (Line (N,2)) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ;
now :: thesis: ( len (Line (N,2)) = 3 & (Line (N,2)) . 1 = N * (2,1) & (Line (N,2)) . 2 = N * (2,2) & (Line (N,2)) . 3 = N * (2,3) )
thus len (Line (N,2)) = 3 by A71; :: thesis: ( (Line (N,2)) . 1 = N * (2,1) & (Line (N,2)) . 2 = N * (2,2) & (Line (N,2)) . 3 = N * (2,3) )
Seg (width N) = Seg 3 by MATRIX_0:23;
hence ( (Line (N,2)) . 1 = N * (2,1) & (Line (N,2)) . 2 = N * (2,2) & (Line (N,2)) . 3 = N * (2,3) ) by FINSEQ_1:1, MATRIX_0:def 7; :: thesis: verum
end;
then A72: Line (N,2) = <*(N * (2,1)),(N * (2,2)),(N * (2,3))*> by FINSEQ_1:45;
reconsider z1 = u1 . 1, z2 = u1 . 2, z3 = u1 . 3, z4 = u2 . 1, z5 = u2 . 2, z6 = u2 . 3 as Element of F_Real by XREAL_0:def 1;
A73: (Line (N,2)) "*" (Col ((<*uf1*> @),1)) = (((N * (2,1)) * z1) + ((N * (2,2)) * z2)) + ((N * (2,3)) * z3) by A72, A67, A70, Th6;
A74: (Line (N,2)) "*" (Col ((<*uf2*> @),1)) = (((N * (2,1)) * z4) + ((N * (2,2)) * z5)) + ((N * (2,3)) * z6) by A68, A72, A70, Th6;
( u1 . 1 = a * (u2 . 1) & u1 . 2 = a * (u2 . 2) & u1 . 3 = a * (u2 . 3) ) by A69, A67, FINSEQ_1:78;
hence (Line (N,2)) "*" (Col ((<*uf1*> @),1)) = a * ((Line (N,2)) "*" (Col ((<*uf2*> @),1))) by A73, A74; :: thesis: verum
end;
hence p1 . 2 = <*(a * q2)*> by A64, FINSEQ_1:40, A65, A29, A66; :: thesis: verum
end;
thus p1 . 3 = <*(a * q3)*> :: thesis: verum
proof
A75: [3,1] in Indices (N * (<*uf2*> @)) by Th2, A34, MATRIX_0:23;
A76: [3,1] in Indices (N * (<*uf1*> @)) by Th2, A32, MATRIX_0:23;
A77: p1 . 3 = (N * (<*uf1*> @)) . 3 by A15, LAPLACE:def 9
.= Line ((N * (<*uf1*> @)),3) by A40, A41, MATRIX_0:52 ;
then A78: len (p1 . 3) = width (N * (<*uf1*> @)) by MATRIX_0:def 7
.= 1 by A40, MATRIX_0:23 ;
A79: (p1 . 3) . 1 = (N * (<*uf1*> @)) * (3,1) by A77, FINSEQ_1:1, A42, MATRIX_0:def 7
.= (Line (N,3)) "*" (Col ((<*uf1*> @),1)) by B01, A26, A76, MATRIX_3:def 4 ;
p2 . 3 = (N * (<*uf2*> @)) . 3 by A21, LAPLACE:def 9
.= Line ((N * (<*uf2*> @)),3) by A43, A44, MATRIX_0:52 ;
then A80: (p2 . 3) . 1 = (N * (<*uf2*> @)) * (3,1) by FINSEQ_1:1, A45, MATRIX_0:def 7
.= (Line (N,3)) "*" (Col ((<*uf2*> @),1)) by B01, A27, A75, MATRIX_3:def 4 ;
(Line (N,3)) "*" (Col ((<*uf1*> @),1)) = a * ((Line (N,3)) "*" (Col ((<*uf2*> @),1)))
proof
( u1 `1 = u1 . 1 & u1 `2 = u1 . 2 & u1 `3 = u1 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A81: u1 = |[(u1 . 1),(u1 . 2),(u1 . 3)]| by EUCLID_5:3;
( u2 `1 = u2 . 1 & u2 `2 = u2 . 2 & u2 `3 = u2 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A82: u2 = |[(u2 . 1),(u2 . 2),(u2 . 3)]| by EUCLID_5:3;
A83: u1 = |[(a * (u2 . 1)),(a * (u2 . 2)),(a * (u2 . 3))]| by A25, A82, EUCLID_5:8;
A84: ( Col ((<*uf1*> @),1) = u1 & Col ((<*uf2*> @),1) = u2 ) by Th76, A14, A20;
A85: len (Line (N,3)) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ;
now :: thesis: ( len (Line (N,3)) = 3 & (Line (N,3)) . 1 = N * (3,1) & (Line (N,3)) . 2 = N * (3,2) & (Line (N,3)) . 3 = N * (3,3) )
thus len (Line (N,3)) = 3 by A85; :: thesis: ( (Line (N,3)) . 1 = N * (3,1) & (Line (N,3)) . 2 = N * (3,2) & (Line (N,3)) . 3 = N * (3,3) )
Seg (width N) = Seg 3 by MATRIX_0:23;
hence ( (Line (N,3)) . 1 = N * (3,1) & (Line (N,3)) . 2 = N * (3,2) & (Line (N,3)) . 3 = N * (3,3) ) by FINSEQ_1:1, MATRIX_0:def 7; :: thesis: verum
end;
then A86: Line (N,3) = <*(N * (3,1)),(N * (3,2)),(N * (3,3))*> by FINSEQ_1:45;
reconsider z1 = u1 . 1, z2 = u1 . 2, z3 = u1 . 3, z4 = u2 . 1, z5 = u2 . 2, z6 = u2 . 3 as Element of F_Real by XREAL_0:def 1;
A87: (Line (N,3)) "*" (Col ((<*uf1*> @),1)) = (((N * (3,1)) * z1) + ((N * (3,2)) * z2)) + ((N * (3,3)) * z3) by A86, A81, A84, Th6;
A88: (Line (N,3)) "*" (Col ((<*uf2*> @),1)) = (((N * (3,1)) * z4) + ((N * (3,2)) * z5)) + ((N * (3,3)) * z6) by A82, A86, A84, Th6;
( u1 . 1 = a * (u2 . 1) & u1 . 2 = a * (u2 . 2) & u1 . 3 = a * (u2 . 3) ) by A83, A81, FINSEQ_1:78;
hence (Line (N,3)) "*" (Col ((<*uf1*> @),1)) = a * ((Line (N,3)) "*" (Col ((<*uf2*> @),1))) by A87, A88; :: thesis: verum
end;
hence p1 . 3 = <*(a * q3)*> by A78, A79, A29, A80, FINSEQ_1:40; :: thesis: verum
end;
end;
hence p1 = <*<*(a * q1)*>,<*(a * q2)*>,<*(a * q3)*>*> by FINSEQ_1:45; :: thesis: verum
end;
hence p1 = a * p2 by A30; :: thesis: verum
end;
a * v2 = M2F (a * p2) by A28, MATRIX_0:23, A22, Th67
.= <*((p1 . 1) . 1),((p1 . 2) . 1),((p1 . 3) . 1)*> by A31, DEF2, A36 ;
hence M2F p1 = a * v2 by A35, DEF2; :: thesis: verum
end;
hence v1 = a * v2 by A16; :: thesis: ( not v1 is zero & not v2 is zero )
thus not v1 is zero by A13, A14, A15, A16, Th82; :: thesis: not v2 is zero
thus not v2 is zero by A19, A20, A21, A22, Th82; :: thesis: verum
end;
then ( are_Prop v1,v2 & not v1 is zero & not v2 is zero ) by A24, ANPROJ_1:1;
hence f1 . x = f2 . x by A17, A23, ANPROJ_1:22; :: thesis: verum
end;
end;
hence f1 = f2 by FUNCT_1:def 11; :: thesis: verum