let n be Nat; :: thesis: for X being set
for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n
let X be set ; :: thesis: for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n
let A1 be SetSequence of X; :: thesis: A1 . n c= (Partial_Union A1) . n
per cases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
suppose n = 0 ; :: thesis: A1 . n c= (Partial_Union A1) . n
hence A1 . n c= (Partial_Union A1) . n by Def2; :: thesis: verum
end;
suppose ex k being Nat st n = k + 1 ; :: thesis: A1 . n c= (Partial_Union A1) . n
then consider k being Nat such that
A1: n = k + 1 ;
(Partial_Union A1) . (k + 1) = ((Partial_Union A1) . k) \/ (A1 . (k + 1)) by Def2;
hence A1 . n c= (Partial_Union A1) . n by A1, XBOOLE_1:7; :: thesis: verum
end;
end;