let R be non degenerated comRing; :: thesis: ex X being Element of (Polynom-Ring R) st
( X is indeterminate & X = 1_1 R )
reconsider X = 1_1 R as Element of (Polynom-Ring R) by POLYNOM3:def 10;
A1: (id (Polynom-Ring R)) . (1_1 R) = X ;
take X ; :: thesis: ( X is indeterminate & X = 1_1 R )
thus ( X is indeterminate & X = 1_1 R ) by A1; :: thesis: verum