let l be Element of the Lines of ; :: thesis: (line_homography (1. (F_Real,3))) . l = l
set X = { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l } ;
A1: { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l } c= l
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l } or x in l )
assume x in { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l } ; :: thesis: x in l
then consider P being POINT of such that
A2: x = (homography (1. (F_Real,3))) . P and
A3: P on l ;
A4: P is Point of real_projective_plane by INCPROJ:2;
then A5: x = P by ;
l is LINE of real_projective_plane by INCPROJ:4;
hence x in l by ; :: thesis: verum
end;
l c= { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in l or x in { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l } )
assume A6: x in l ; :: thesis: x in { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l }
A7: l is LINE of real_projective_plane by INCPROJ:4;
l is Subset of real_projective_plane by INCPROJ:4;
then reconsider x9 = x as Point of real_projective_plane by A6;
reconsider l9 = l as LINE of ;
reconsider x99 = x9 as POINT of by INCPROJ:3;
A8: x99 on l by ;
(homography (1. (F_Real,3))) . x99 = x99 by ANPROJ_9:14;
hence x in { ((homography (1. (F_Real,3))) . P) where P is POINT of : P on l } by A8; :: thesis: verum
end;
hence (line_homography (1. (F_Real,3))) . l = l by ; :: thesis: verum