A1: dom X = I by PARTFUN1:def 2;

per cases ( I = {} or I <> {} ) ;

suppose I = {} ; :: thesis: X . i is Component of X

hence X . i is Component of X by SUBSET_1:def 1; :: thesis: verum

end;

suppose I <> {} ; :: thesis: X . i is Component of X

hence X . i is Component of X by A1, FUNCT_1:def 3; :: thesis: verum

end;

end;