let R be domRing; :: thesis: for n being non empty Ordinal holds Zero_ (0_ (n,R)) = Funcs (n,([#] R))
let n be non empty Ordinal; :: thesis: Zero_ (0_ (n,R)) = Funcs (n,([#] R))
for o being object st o in Funcs (n,([#] R)) holds
o in Zero_ (0_ (n,R))

proof

let o be object ; :: thesis: ( o in Funcs (n,([#] R)) implies o in Zero_ (0_ (n,R)) )
assume o in Funcs (n,([#] R)) ; :: thesis: o in Zero_ (0_ (n,R))
then consider x being Function such that
A2: ( o = x & dom x = n & rng x c= [#] R ) by FUNCT_2:def 2;
reconsider x = x as Function of n,R by A2, FUNCT_2:2;
eval ((0_ (n,R)),x) = 0. R by POLYNOM2:20;
hence o in Zero_ (0_ (n,R)) by A2; :: thesis: verum

end;

then Funcs (n,([#] R)) c= Zero_ (0_ (n,R)) ;
hence Zero_ (0_ (n,R)) = Funcs (n,([#] R)) ; :: thesis: verum