let T be non empty RelStr ; :: thesis: for A, B being Subset of T
for n being Element of NAT holds Fcl (A \/ B),n = (Fcl A,n) \/ (Fcl B,n)
let A, B be Subset of T; :: thesis: for n being Element of NAT holds Fcl (A \/ B),n = (Fcl A,n) \/ (Fcl B,n)
A1: for n being Element of NAT holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n)

proof

defpred S₁[ Element of NAT ] means (Fcl (A \/ B)) . $1 = ((Fcl A) . $1) \/ ((Fcl B) . $1);
A2: S₁[ 0 ]

proof

(Fcl (A \/ B)) . 0 = A \/ B by Def2
.= ((Fcl A) . 0 ) \/ B by Def2
.= ((Fcl A) . 0 ) \/ ((Fcl B) . 0 ) by Def2 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
(Fcl (A \/ B)) . (k + 1) = (Fcl (A \/ B),k) ^b by Def2
.= ((Fcl A,k) ^b ) \/ ((Fcl B,k) ^b ) by A4, Th8
.= (Fcl A,(k + 1)) \/ ((Fcl B,k) ^b ) by Def2
.= ((Fcl A) . (k + 1)) \/ ((Fcl B) . (k + 1)) by Def2 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence for n being Element of NAT holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n) ; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: Fcl (A \/ B),n = (Fcl A,n) \/ (Fcl B,n)
thus Fcl (A \/ B),n = (Fcl A,n) \/ (Fcl B,n) by A1; :: thesis: verum