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