let I, J be non empty set ; for a being Function of I,J
for F being Group-Family of J
for x being Function holds a .: (support ((x * a),(F * a))) c= support (x,F)
let a be Function of I,J; for F being Group-Family of J
for x being Function holds a .: (support ((x * a),(F * a))) c= support (x,F)
let F be Group-Family of J; for x being Function holds a .: (support ((x * a),(F * a))) c= support (x,F)
let x be Function; a .: (support ((x * a),(F * a))) c= support (x,F)
for j being object st j in a .: (support ((x * a),(F * a))) holds
j in support (x,F)
proof
let j be
object ;
( j in a .: (support ((x * a),(F * a))) implies j in support (x,F) )
assume
j in a .: (support ((x * a),(F * a)))
;
j in support (x,F)
then consider i being
object such that A1:
i in dom a
and A2:
i in support (
(x * a),
(F * a))
and A3:
j = a . i
by FUNCT_1:def 6;
consider Z being
Group such that B1:
(
Z = (F * a) . i &
(x * a) . i <> 1_ Z &
i in I )
by A2, GROUP_19:def 1;
reconsider y =
x * a as
Function ;
reconsider G =
F * a as
Group-Family of
I ;
reconsider i =
i as
Element of
I by B1;
j = a . i
by A3;
then reconsider j =
j as
Element of
J ;
A5:
1_ (G . i) = 1_ (F . j)
by A1, A3, FUNCT_1:13;
x . j <> 1_ (F . j)
by A1, A3, B1, A5, FUNCT_1:13;
hence
j in support (
x,
F)
by GROUP_19:def 1;
verum
end;
hence
a .: (support ((x * a),(F * a))) c= support (x,F)
; verum