let R be non degenerated comRing; :: thesis: Support (1_1 R) = {1}
A1: for o being object st o in Support (1_1 R) holds
o in {1}

proof

let o be object ; :: thesis: ( o in Support (1_1 R) implies o in {1} )
assume A2: o in Support (1_1 R) ; :: thesis: o in {1}
then reconsider x = o as Element of NAT ;
x = 1

proof

assume x <> 1 ; :: thesis: contradiction
then ((0_. R) +* (1,(1. R))) . x = (0_. R) . x by FUNCT_7:32
.= 0. R ;
hence contradiction by A2, POLYNOM1:def 4; :: thesis: verum

end;

hence o in {1} by TARSKI:def 1; :: thesis: verum

end;

for o being object st o in {1} holds
o in Support (1_1 R)

proof

let o be object ; :: thesis: ( o in {1} implies o in Support (1_1 R) )
assume A4: o in {1} ; :: thesis: o in Support (1_1 R)
then A5: o = 1 by TARSKI:def 1;
A6: o in dom (0_. R) by A4;
then A7: o in dom ((0_. R) +* (1,(1. R))) by FUNCT_7:30;
((0_. R) +* (1,(1. R))) . o = 1. R by A5, A6, FUNCT_7:31;
hence o in Support (1_1 R) by A7, POLYNOM1:def 3; :: thesis: verum

end;

hence Support (1_1 R) = {1} by A1, TARSKI:2; :: thesis: verum