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 st a is one-to-one 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 st a is one-to-one holds
a .: (support ((x * a),(F * a))) c= support (x,F)
let F be Group-Family of J; for x being Function st a is one-to-one holds
a .: (support ((x * a),(F * a))) c= support (x,F)
let x be Function; ( a is one-to-one implies a .: (support ((x * a),(F * a))) c= support (x,F) )
assume
a is one-to-one
; 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;
reconsider y =
x * a as
Function ;
reconsider G =
F * a as
Group-Family of
I ;
A4:
y . i <> 1_ (G . i)
by A2, GROUP_19:def 1;
A5:
1_ (G . i) = 1_ (F . j)
by A1, A3, FUNCT_1:13;
A6:
x . j <> 1_ (F . j)
by A1, A3, A4, A5, FUNCT_1:13;
j in rng a
by A1, A3, FUNCT_1:def 3;
hence
j in support (
x,
F)
by A6, GROUP_19:def 1;
verum
end;
hence
a .: (support ((x * a),(F * a))) c= support (x,F)
; verum