let R be domRing; for n being non empty Ordinal
for m being non zero Nat
for P being Subset of (singletons (Funcs (n,([#] R)))) st card P = m holds
union P is Algebraic_Set of n,R
let n be non empty Ordinal; for m being non zero Nat
for P being Subset of (singletons (Funcs (n,([#] R)))) st card P = m holds
union P is Algebraic_Set of n,R
let m be non zero Nat; for P being Subset of (singletons (Funcs (n,([#] R)))) st card P = m holds
union P is Algebraic_Set of n,R
let P be Subset of (singletons (Funcs (n,([#] R)))); ( card P = m implies union P is Algebraic_Set of n,R )
assume A1:
card P = m
; union P is Algebraic_Set of n,R
A2:
singletons (Funcs (n,([#] R))) c= Alg_Sets (n,R)
proof
for
o being
object st
o in singletons (Funcs (n,([#] R))) holds
o in Alg_Sets (
n,
R)
proof
let o be
object ;
( o in singletons (Funcs (n,([#] R))) implies o in Alg_Sets (n,R) )
assume
o in singletons (Funcs (n,([#] R)))
;
o in Alg_Sets (n,R)
then
o in { S where S is Subset of (Funcs (n,([#] R))) : S is 1 -element }
by BSPACE:def 8;
then consider S being
Subset of
(Funcs (n,([#] R))) such that A4:
(
o = S &
S is 1
-element )
;
consider p being
Element of
Funcs (
n,
([#] R))
such that A5:
S = {p}
by A4, CARD_1:65;
S is
Algebraic_Set of
n,
R
by A5, Th26;
hence
o in Alg_Sets (
n,
R)
by A4;
verum
end;
hence
singletons (Funcs (n,([#] R))) c= Alg_Sets (
n,
R)
;
verum
end;
P c= Alg_Sets (n,R)
by A2;
hence
union P is Algebraic_Set of n,R
by A1, Th24; verum