let X be set ; :: thesis: for A, B being Subset of X holds Complement (A followed_by B) = (A ` ) followed_by (B ` )
let A, B be Subset of X; :: thesis: Complement (A followed_by B) = (A ` ) followed_by (B ` )
let n be Element of NAT ; :: according to FUNCT_2:def 9 :: thesis: (Complement (A followed_by B)) . n = ((A ` ) followed_by (B ` )) . n

per cases ( n = 0 or n > 0 ) by NAT_1:3;

suppose A1: n = 0 ; :: thesis: (Complement (A followed_by B)) . n = ((A ` ) followed_by (B ` )) . n

thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def4
.= A ` by A1, FUNCT_7:121
.= ((A ` ) followed_by (B ` )) . n by A1, FUNCT_7:121 ; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: (Complement (A followed_by B)) . n = ((A ` ) followed_by (B ` )) . n

thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def4
.= B ` by A2, FUNCT_7:122
.= ((A ` ) followed_by (B ` )) . n by A2, FUNCT_7:122 ; :: thesis: verum

end;

end;